This site uses cookies to deliver our services and to ensure you get the best experience. By continuing to use this site, you consent to our use of cookies and acknowledge that you have read and understand our Privacy Policy, Cookie Policy, and Terms
The objective of this paper is to develop a functional programming language for quantum computers. We develop a lambda calculus for the classical control model, following the firs...
αProlog is a logic programming language which is well-suited for rapid prototyping of type systems and operational semantics of typed λ-calculi and many other languages involving...
Two common misbeliefs about encodings of the λ-calculus in interaction nets (INs) are that they are good only for strategies that are not very well understood (e.g. optimal reduct...
This paper studies continuity of the normal form and the context operators as functions in the infinitary lambda calculus. We consider the Scott topology on the cpo of the finite...
Abstract. The Focal language (formerly FoC) allows one to incrementally build modules and to formally prove their correctness. In this paper, we present two formal semantics for en...
We explore foundational typing support for strong updates — updating a memory cell to hold values of unrelated types at different points in time. We present a simple, but expres...
This work sets the formal bases for building tools that help retrieve classes in object-oriented libraries. In such systems, the user provides a query, formulated as a set of class...
Abstract. We present a theory of proof denotations in classical propologic. The abstract definition is in terms of a semiring of weights, and two concrete instances are explored. ...