The elementary affine lambda-calculus was introduced as a polyvalent setting for implicit computational complexity, allowing for characterizations of polynomial time and hyperexponential time predicates. But these results rely on type fixpoints (a.k.a. recursive types), and it was unknown whether this feature of the type system was really necessary. We give a positive answer by showing that without type fixpoints, we get a characterization of regular languages instead of polynomial time. The proof uses the semantic evaluation method. We also propose an aesthetic improvement on the characterization of the function classes FP and k-FEXPTIME in the presence of recursive types.
Cartesian difference categories are a recent generalisation of Cartesian differential categories which introduce a notion of "infinitesimal" arrows satisfying an analogue of the Kock-Lawvere axiom, with the axioms of a Cartesian differential category being satisfied only "up to an infinitesimal perturbation". In this work, we construct a simply-typed calculus in the spirit of the differential lambda-calculus equipped with syntactic infinitesimals and show how its models correspond to difference lambda-categories, a family of Cartesian difference categories equipped with suitably well-behaved e…
We propose an intersection type system for an imperative lambda-calculus based on a state monad and equipped with algebraic operations to read and write to the store. The system is derived by solving a suitable domain equation in the category of omega-algebraic lattices; the solution consists of a filter-model generalizing the well-known construction for ordinary lambda-calculus. Then the type system is obtained out of the term interpretations into the filter-model itself. The so obtained type system satisfies the "type-semantics" property, and it is sound and complete by construction.
A notion of probabilistic lambda-calculus usually comes with a prescribed reduction strategy, typically call-by-name or call-by-value, as the calculus is non-confluent and these strategies yield different results. This is a break with one of the main advantages of lambda-calculus: confluence, which means results are independent from the choice of strategy. We present a probabilistic lambda-calculus where the probabilistic operator is decomposed into two syntactic constructs: a generator, which represents a probabilistic event; and a consumer, which acts on the term depending on a given event. …
A new, comprehensive approach to inhabitation problems in simply-typed lambda-calculus is shown, dealing with both decision and counting problems. This approach works by exploiting a representation of the search space generated by a given inhabitation problem, which is in terms of a lambda-calculus for proof search that the authors developed recently. The representation may be seen as extending the Curry-Howard representation of proofs by lambda-terms, staying within the methods of lambda-calculus and type systems. Our methodology reveals inductive descriptions of the decision problems, driven…
We formally verify an abstract machine for a call-by-value lambda-calculus with de Bruijn terms, simple substitution, and small-step semantics. We follow a stepwise refinement approach starting with a naive stack machine with substitution. We then refine to a machine with closures, and finally to a machine with a heap providing structure sharing for closures. We prove the correctness of the three refinement steps with compositional small-step bottom-up simulations. There is an accompanying Coq development verifying all results.
We present the guarded lambda-calculus, an extension of the simply typed lambda-calculus with guarded recursive and coinductive types. The use of guarded recursive types ensures the productivity of well-typed programs. Guarded recursive types may be transformed into coinductive types by a type-former inspired by modal logic and Atkey-McBride clock quantification, allowing the typing of acausal functions. We give a call-by-name operational semantics for the calculus, and define adequate denotational semantics in the topos of trees. The adequacy proof entails that the evaluation of a program alw…
We give a semantics for the lambda-calculus based on a topological duality theorem in nominal sets. A novel interpretation of lambda is given in terms of adjoints, and lambda-terms are interpreted absolutely as sets (no valuation is necessary).
本文对Manzonetto博士论文中关于纯无类型代数演算的指称语义和等式/序理论的内容作了简要的总结。主要的研究成果包括：（1）从自反对象构造了一个一般的自反模型，（可能非适点）范畴;（ii）组合代数的斯通式表示定理;（iii）证明没有有效的Eudda模型可以有Euda-beta或Euda-beta-eta作为其方程理论（这可以被看作是对Honsell-Ronchi Della Rocca在1984年提出的一个开放问题的部分回答）。
We present a model of Selinger and Valiron's quantum lambda calculus based on von Neumann algebras, and show that the model is adequate with respect to the operational semantics.
We have previously published the Isabelle/HOL formalization of a general theory of syntax with bindings. In this companion paper, we instantiate the general theory to the syntax of lambda-calculus and formalize the development leading to several fundamental constructions and results: sound semantic interpretation, the Church-Rosser and standardization theorems, and higher-order abstract syntax (HOAS) encoding. For Church-Rosser and standardization, our work covers both the call-by-name and call-by-value versions of the calculus, following classic papers by Takahashi and Plotkin. During the for…
We revisit the Vectorial Lambda Calculus, a typed version of Lineal. Vectorial (as well as Lineal) has been originally designed for quantum computing, as an extension to System F where linear combinations of lambda terms are also terms and linear combinations of types are also types. In its first presentation, Vectorial only provides a weakened version of the Subject Reduction property. We prove that our revised Vectorial Lambda Calculus supports the standard version of said property, answering a long standing issue. In addition we also introduce the concept of weight of types and terms, and p…
超级演绎是一种专门设计的方法，以简化谓词逻辑中一阶理论的使用。运用这一理论，以系统、正确、完整的方式，用新的演绎规则丰富演绎体系。一个证明项语言和一个切消约化已经存在于超演绎中，两者都是基于克里斯蒂安·厄本在经典微积分上的工作。然而，克里斯蒂安·厄本的微积分的计算内容与柯里-霍华德对应（Curry-Howard correspondence）没有直接关系。相反，Lambda bar mu mu波浪线演算是经典波浪线演算的一种波浪线演算。这个简短的文件是第一步，进一步探索的计算内容的superdeduction证明，我们延长了Lambda酒吧亩亩波浪演算，以获得一个proofterm语言一起削减消除减少superdeduction。我们还证明了强大的规范化，这种扩展的λ酒吧亩亩波浪演算。
We define sound and adequate denotational and operational semantics for the stochastic lambda calculus. These two semantic approaches build on previous work that used similar techniques to reason about higher-order probabilistic programs, but for the first time admit an adequacy theorem relating the operational and denotational views. This resolves the main issue left open in (Bacci et al. 2018).
