The Semantics of Local Storage of What Makes The Free-list Free? by Halpern, Joseph Y., Meyer, Albert R., Trakhtenbrot, B.A.

“…Denotational semantics for an ALGOL-like language with finite-mode procedures, blocks with local storage, and sharing (aliasing) is given by translating programs into an appropriately typed lambda-calculus. Procedures are entirely explained at a purely functional level - independent of the interpretation of program constructs - by continuous models for lambda-calculus. …”
Get full text

Proving Soundness of Extensional Normal-Form Bisimilarities by Dariusz Biernacki, Serguei Lenglet, Piotr Polesiuk

“…We illustrate our technique with three calculi: the call-by-value $\lambda$-calculus, the call-by-value $\lambda$-calculus with the delimited-control operators shift and reset, and the call-by-value $\lambda$-calculus with the abortive control operators call/cc and abort. …”
Get full text

Gems of Corrado B\"ohm by Henk P. Barendregt

“…Self-evaluation in {\lambda}-calculus.…”
Get full text

Initial Semantics for Reduction Rules by Benedikt Ahrens

“…By equipping the untyped lambda calculus with the structure of a model of PCF, initiality yields a translation from PCF to the lambda calculus, that is faithful with respect to the reduction semantics specified by the rules. …”
Get full text

A correspondence between rooted planar maps and normal planar lambda terms by Noam Zeilberger, Alain Giorgetti

“…A term of the pure lambda calculus is said to be linear if every variable is used exactly once, normal if it contains no beta-redexes, and planar if it is linear and the use of variables moreover follows a deterministic stack discipline. …”
Get full text

The Complexity of Model Checking Higher-Order Fixpoint Logic by Roland Axelsson, Martin Lange, Rafal Somla

“…Higher-Order Fixpoint Logic (HFL) is a hybrid of the simply typed \lambda-calculus and the modal \lambda-calculus. This makes it a highly expressive temporal logic that is capable of expressing various interesting correctness properties of programs that are not expressible in the modal \lambda-calculus. …”
Get full text

Observational Equivalence and Full Abstraction in the Symmetric Interaction Combinators by Damiano Mazza

“…This is obtained by interpreting nets as certain subsets of the Cantor space, called edifices, which play the same role as Boehm trees in the theory of the lambda-calculus.…”
Get full text

Learning to map sentences to logical form by Zettlemoyer, Luke S. (Luke Sean), 1978-

Get full text

A categorical framework for congruence of applicative bisimilarity in higher-order languages by Tom Hirschowitz, Ambroise Lafont

“…Applicative bisimilarity is a coinductive characterisation of observational equivalence in call-by-name lambda-calculus, introduced by Abramsky (1990). Howe (1996) gave a direct proof that it is a congruence, and generalised the result to all languages complying with a suitable format. …”
Get full text

Modules over monads and operational semantics (expanded version) by André Hirschowitz, Tom Hirschowitz, Ambroise Lafont

“…Generalising the reduction monads of Ahrens et al., we introduce transition monads, thus covering new applications such as lambda-bar-mu-calculus, pi-calculus, Positive GSOS specifications, differential lambda-calculus, and the big-step, simply-typed, call-by-value lambda-calculus. …”
Get full text

On the Relation of Interaction Semantics to Continuations and Defunctionalization by Ulrich Schöpp

“…We then establish a relation between these two compilation methods for the simply-typed {\lambda}-calculus and end by considering recursion.…”
Get full text

The Semantics of Miranda's Algebraic Types by Bruce, Kim B., Riecker, Jon G.

“…We first define a typed lambda calculus that specifies type constructors. A semantic model of type constructors is them built, using the ideal model as a basis. …”
Get full text

Towards a categorical foundation for generic programming by Hinze, R, Wu, N

“…Since types in Haskell include parametric types such as `list of', Generic Haskell represents types by terms of the simply-typed lambda calculus. This paper puts the idea of interpreting types as functions on a firm theoretical footing, exploiting the fact that the simply-typed lambda calculus can be interpreted in a cartesian closed category. …”

Quantum Control in the Unitary Sphere: Lambda-S1 and its Categorical Model by Alejandro Díaz-Caro, Octavio Malherbe

“…In a recent paper, a realizability technique has been used to give a semantics of a quantum lambda calculus. Such a technique gives rise to an infinite number of valid typing rules, without giving preference to any subset of those. …”
Get full text

Solvability = Typability + Inhabitation by Antonio Bucciarelli, Delia Kesner, Simona Ronchi Della Rocca

“…We extend the classical notion of solvability to a lambda-calculus equipped with pattern matching. We prove that solvability can be characterized by means of typability and inhabitation in an intersection type system P based on non-idempotent types. …”
Get full text

Towards a Categorical Foundation for Generic Programming by Hinze, R, Wu, N, ACM

“…Since types in Haskell include parametric types such as 'list of', Generic Haskell represents types by terms of the simply-typed lambda calculus. This paper puts the idea of interpreting types as functions on a firm theoretical footing, exploiting the fact that the simply-typed lambda calculus can be interpreted in a cartesian closed category. …”

Modular coinduction up-to for higher-order languages via first-order transition systems by Jean-Marie Madiot, Damien Pous, Davide Sangiorgi

“…We investigate the method on the pi-calculus, the lambda-calculus, and a (call-by-value) lambda-calculus with references.…”
Get full text

On the enumeration of closures and environments with an application to random generation by Maciej Bendkowski, Pierre Lescanne

“…Environments and closures are two of the main ingredients of evaluation in lambda-calculus. A closure is a pair consisting of a lambda-term and an environment, whereas an environment is a list of lambda-terms assigned to free variables. …”
Get full text

A Rewriting View of Simple Typing by Aaron Stump, Garrin Kimmell, Hans Zantema, Ruba El Haj Omar

“…Finally, we show how to adapt a standard proof of normalization of simply typed lambda calculus, for the rewriting approach to typing.…”
Get full text

Relational Graph Models at Work by Flavien Breuvart, Giulio Manzonetto, Domenico Ruoppolo

“…We study the relational graph models that constitute a natural subclass of relational models of lambda-calculus. We prove that among the lambda-theories induced by such models there exists a minimal one, and that the corresponding relational graph model is very natural and easy to construct. …”
Get full text