Related papers: Open Call-by-Value (Extended Version)
Calculational abstract interpretation, long advocated by Cousot, is a technique for deriving correct-by-construction abstract interpreters from the formal semantics of programming languages. This paper addresses the problem of deriving…
We prove the Stability Property for the call-by-value $\lambda$-calculus (CbV in the following). This result states necessary conditions under which the contexts of the CbV $\lambda$-calculus commute with intersections of approximants. This…
The $\lambda$-calculus is a handy formalism to specify the evaluation of higher-order programs. It is not very handy, however, when one interprets the specification as an execution mechanism, because terms can grow exponentially with the…
Programming languages are expected to support programmer's effort to structure program code. The ML module system, object systems and mixins are good examples of language constructs promoting modular programming. Among the three, mixins can…
We define an extension of lambda-calculus with dependents types that enables us to encode transparent and opaque probabilistic programs and prove a strong normalisation result for it by a reducibility technique. While transparent…
Proof search has been used to specify a wide range of computation systems. In order to build a framework for reasoning about such specifications, we make use of a sequent calculus involving induction and co-induction. These proof principles…
Auto-active program verification rests on the ability to effectively the translation from annotated programs into verification conditions that are then discharged by automated theorem provers in the background. Characteristic such tools,…
Normal-form bisimilarity is a simple, easy-to-use behavioral equivalence that relates terms in $\lambda$-calculi by decomposing their normal forms into bisimilar subterms. Moreover, it typically allows for powerful up-to techniques, such as…
This paper is a concise and painless introduction to the $\lambda$-calculus. This formalism was developed by Alonzo Church as a tool for studying the mathematical properties of effectively computable functions. The formalism became popular…
Object-oriented programming (OOP) is one of the most popular paradigms used for building software systems. However, despite its industrial and academic popularity, OOP is still missing a formal apparatus similar to \(\lambda\)-calculus,…
Reasoning about the cost of executing programs is one of the fundamental questions in computer science. In the context of programming with probabilities, however, the notion of cost stops being deterministic, since it depends on the…
In functional programming, point-free relation calculi have been fruitful for general theories of program construction, but for specific applications pointwise expressions can be more convenient and comprehensible. In imperative…
We present the first fully abstract normal form bisimulation for call-by-value PCF (PCF$_{\textsf{v}}$). Our model is based on a labelled transition system (LTS) that combines elements from applicative bisimulation, environmental…
We consider lambda-Y-calculus as a non-interpreted functional programming language: the result of the execution of a program is its normal form that can be seen as the tree of calls to built-in operations. Weak monadic second-order logic…
In CSL-LICS 2014, Accattoli and Dal Lago showed that there is an implementation of the ordinary (i.e. strong, pure, call-by-name) $\lambda$-calculus into models like RAM machines which is polynomial in the number of $\beta$-steps, answering…
This paper formalizes and proves correct a compilation scheme for mutually-recursive definitions in call-by-value functional languages. This scheme supports a wider range of recursive definitions than previous methods. We formalize our…
The algebraic lambda calculus and the linear algebraic lambda calculus are two extensions of the classical lambda calculus with linear combinations of terms. They arise independently in distinct contexts: the former is a fragment of the…
We provide a sound and relatively complete Hoare-like proof system for reasoning about partial correctness of recursive procedures in presence of local variables and the call-by-value parameter mechanism, and in which the correctness proofs…
We adapt Fiore, Plotkin, and Turi's treatment of abstract syntax with binding, substitution, and holes to account for languages with second-class sorts. These situations include programming calculi such as the Call-by-Value lambda-calculus…
The sequent calculus is a proof system which was designed as a more symmetric alternative to natural deduction. The {\lambda}{\mu}{\mu}-calculus is a term assignment system for the sequent calculus and a great foundation for compiler…