Semantical Paradigms: Notes for an Invited Lecture by Meyer, Albert R., Cosmadakis, Stavros S.

“…For readers impatient with sketchy overviews, two appendices mostly by Cosmadakis provide the key parts of a long proof that Scott domains give a computationally adequate and fully abstract semantics for lambda calculus with simple recursive types.…”
Get full text

Normalization of IZF with Replacement by Wojciech Moczydlowski

“…We define a typed lambda calculus $\li$ corresponding to proofs in \iizfr according to the Curry-Howard isomorphism principle. …”
Get full text

Relational Parametricity and Control by Masahito Hasegawa

“…We study the equational theory of Parigot's second-order λμ-calculus in connection with a call-by-name continuation-passing style (CPS) translation into a fragment of the second-order λ-calculus. It is observed that the relational parametricity on the target calculus induces a natural notion of equivalence on the λμ-terms. …”
Get full text

Rank 2 Type Systems and Recursive Definitions by Jim, Trevor

“…We demonstrate an equivalence between the rank 2 fragments of the polymorphic lambda calculus (System F) and the intersection type discipline: exactly the same terms are typable in each system. …”
Get full text

On Natural Deduction for Herbrand Constructive Logics I: Curry-Howard Correspondence for Dummett's Logic LC by Federico Aschieri

“…We present a natural deduction and a Curry-Howard correspondence for first-order and second-order Dummett's logic. We add to the lambda calculus an operator which represents, from the viewpoint of programming, a mechanism for representing parallel computations and communication between them, and from the viewpoint of logic, Dummett's axiom. …”
Get full text

On the characterization of models of H*: The semantical aspect by Flavien Breuvart

“…We give a characterization, with respect to a large class of models of untyped lambda-calculus, of those models that are fully abstract for head-normalization, i.e., whose equational theory is H* (observations for head normalization). …”
Get full text

Differentials and distances in probabilistic coherence spaces by Thomas Ehrhard

“…This suggests that extending probabilistic programming languages with derivatives, in the spirit of the differential lambda-calculus, could be quite meaningful.…”
Get full text

Monads need not be endofunctors by Thosten Altenkirch, James Chapman, Tarmo Uustalu

“…Examples include finite-dimensional vector spaces, untyped and typed lambda-calculus syntax and indexed containers. We show that the Kleisli and Eilenberg-Moore constructions carry over to relative monads and are related to relative adjunctions. …”
Get full text

A Theory of Explicit Substitutions with Safe and Full Composition by Delia Kesner

“…Then, very simple technology in named variable-style notation is used to establish a theory of explicit substitutions for the lambda-calculus which enjoys a whole set of useful properties such as full composition, simulation of one-step beta-reduction, preservation of beta-strong normalisation, strong normalisation of typed terms and confluence on metaterms. …”
Get full text

Asymptotically almost all \lambda-terms are strongly normalizing by René David, Katarzyna Grygiel, Jakub Kozik, Christophe Raffalli, Guillaume Theyssier, Marek Zaionc

“…Surprisingly, in combinatory logic (the translation of the \lambda-calculus into combinators), the result is exactly opposite. …”
Get full text

Strong normalisation for applied lambda calculi by Ulrich Berger

“…We consider the untyped lambda calculus with constructors and recursively defined constants. …”
Get full text

On the Computation Power of Name Parameterization in Higher-order Processes by Xian Xu, Qiang Yin, Huan Long

“…Parameterization extends higher-order processes with the capability of abstraction (akin to that in lambda-calculus), and is known to be able to enhance the expressiveness. …”
Get full text

An estimation for the lengths of reduction sequences of the $\lambda\mu\rho\theta$-calculus by Péter Battyányi, Karim Nour

“…In this paper, based on the result of Xi presented for the $\lambda$-calculus Xi, we give an upper bound for the lengths of the reduction sequences in the $\lambda\mu$-calculus extended with the $\rho$- and $\theta$-rules. …”
Get full text

Non-Deterministic Functions as Non-Deterministic Processes (Extended Version) by Joseph W. N. Paulus, Daniele Nantes-Sobrinho, Jorge A. Pérez

“…We study encodings of the lambda-calculus into the pi-calculus in the unexplored case of calculi with non-determinism and failures. …”
Get full text

Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic by Beniamino Accattoli

“…One of the key properties of the LSC is that it naturally models the sub-term property of abstract machines, that is the key ingredient for the study of reasonable time cost models for the $\lambda$-calculus. The new ESC is then used to design a cut elimination strategy with the sub-term property, providing the first polynomial cost model for cut elimination with unconstrained exponentials. …”
Get full text

Linear Dependent Types and Relative Completeness by Ugo Dal Lago, Marco Gaboardi

“…A system of linear dependent types for the lambda calculus with full higher-order recursion, called dlPCF, is introduced and proved sound and relatively complete. …”
Get full text

Logical relations for coherence of effect subtyping by Dariusz Biernacki, Piotr Polesiuk

“…To illustrate the effectiveness of the proof method, we develop a proof of coherence of a type-directed, selective CPS translation from a typed call-by-value lambda calculus with delimited continuations and control-effect subtyping. …”
Get full text

On tiered small jump operators by Jean-Yves Marion

“…Lastly, we suggest a dependent typed lambda-calculus to represent this construction.…”
Get full text

Stateful Realizers for Nonstandard Analysis by Bruno Dinis, Étienne Miquey

“…In particular, we consider an extension of the $\lambda$-calculus with a memory cell, that contains an integer (the state), in order to indicate in which slice of the ultrapower $\cal{M}^{\mathbb{N}}$ the computation is being done. …”
Get full text

Verification of Ptime Reducibility for system F Terms: Type Inference in Dual Light Affine Logic by Vincent Atassi, Patrick Baillot, Kazushige Terui

“…In a previous work Baillot and Terui introduced Dual light affine logic (DLAL) as a variant of Light linear logic suitable for guaranteeing complexity properties on lambda calculus terms: all typable terms can be evaluated in polynomial time by beta reduction and all Ptime functions can be represented. …”
Get full text