Proving Noninterference by a Fully Complete Translation to the Simply Typed lambda-calculus by Naokata Shikuma, Atsushi Igarashi

“…In this article, instead of DCC, we prove noninterference for sealing calculus, a new variant of DCC, by reduction to the basic lemma of a logical relation for the simply typed lambda-calculus, using a fully complete translation to the simply typed lambda-calculus. …”
Get full text

Nominal Henkin Semantics: simply-typed lambda-calculus models in nominal sets by Murdoch J. Gabbay, Dominic P. Mulligan

“…We investigate a class of nominal algebraic Henkin-style models for the simply typed lambda-calculus in which variables map to names in the denotation and lambda-abstraction maps to a (non-functional) name-abstraction operation. …”
Get full text

On Correspondence between Selective CPS Transformation and Selective Double Negation Translation by Hyeonseung Im

Subjects: 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. …”

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. …”

Investigations on the dual calculus by Tzevelekos, N

“…</p> <p>This paper initially investigates relations of the Dual Calculus to other calculi, namely the simply-typed lambda calculus and the Symmetric lambda calculus. …”

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

Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi by Jose Espirito Santo, Ralph Matthes, Luis Pinto

“…The intuitionistic fragment of the call-by-name version of Curien and Herbelin's \lambda\_mu\_{\~mu}-calculus is isolated and proved strongly normalising by means of an embedding into the simply-typed lambda-calculus. Our embedding is a continuation-and-garbage-passing style translation, the inspiring idea coming from Ikeda and Nakazawa's translation of Parigot's \lambda\_mu-calculus. …”
Get full text

The Safe Lambda Calculus by Blum, W, Ong, C

“…In this paper, we introduce the safe lambda calculus, which is obtained by transposing (and generalizing) the safety condition to the setting of the simply-typed lambda calculus. In contrast to the original definition of safety, our calculus does not constrain types (to be homogeneous). …”

Polytypic values possess polykinded types by Hinze, R

“…Haskell's type system essentially corresponds to the simply typed lambda calculus with kinds playing the role of types. …”

The Safe Lambda Calculus by William Blum, C. -H. Luke Ong

“…In this paper, we introduce the safe lambda calculus, which is obtained by transposing (and generalizing) the safety condition to the setting of the simply-typed lambda calculus. In contrast to the original definition of safety, our calculus does not constrain types (to be homogeneous). …”
Get full text

From Mathematics to Abstract Machine: A formal derivation of an executable Krivine machine by Wouter Swierstra

“…This paper presents the derivation of an executable Krivine abstract machine from a small step interpreter for the simply typed lambda calculus in the dependently typed programming language Agda.…”
Get full text

From Linear Logic to Cyclic Sharing by Masahito Hasegawa

“…We present a translation from Multiplicative Exponential Linear Logic to a simply-typed lambda calculus with cyclic sharing. This translation is derived from a simple observation on the Int-construction on traced monoidal categories. …”
Get full text

Termination in a Pi-calculus with Subtyping by Daniel Hirschkoff, Ioana Cristescu

“…We demonstrate how our system can be extended to handle the encoding of the simply typed lambda-calculus, and discuss questions related to type inference.…”
Get full text

Hereditary Substitution for the λΔ-Calculus by Harley Eades, Aaron Stump

“…We show that there is a non-trivial extension of the hereditary substitution function of the simply-typed lambda calculus to one for the lambda-Delta calculus. …”
Get full text

Reconciling positional and nominal binding by Davide Ancona, Paola Giannini, Elena Zucca

“…We define an extension of the simply-typed lambda calculus where two different binding mechanisms, by position and by name, nicely coexist. …”
Get full text

Classical Proofs as Parallel Programs by Federico Aschieri, Agata Ciabattoni, Francesco Antonio Genco

“…We define a parallel and more powerful extension of the simply typed lambda calculus corresponding to an analytic natural deduction based on the excluded middle law. …”
Get full text

The safe lambda calculus by Blum, W

“…We transpose and generalize this restriction to the setting of the simply-typed lambda calculus, giving rise to what we call the safe lambda calculus. …”

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

Coherence for bicategorical cartesian closed structure by Fiore, M, Saville, P

“…The argument we employ is reminiscent of that used by Čubrić, Dybjer, and Scott to show normalisation for the simply-typed lambda calculus (Čubrić et al., 1998). The main results first appeared in a conference paper (Fiore and Saville, 2020) but for reasons of space many details are omitted there; here we provide the full development.…”