scholarly journals Explaining the lazy Krivine machine using explicit substitution and addresses

2007 ◽  
Vol 20 (3) ◽  
pp. 257-270 ◽  
Author(s):  
Frédéric Lang
Keyword(s):  
Explicit Substitution ◽  
Krivine Machine

Pure type systems with explicit substitution

2001 ◽  
Vol 11 (1) ◽  
pp. 3-19 ◽  
Author(s):  
ROEL BLOO
Keyword(s):  
Type Systems ◽  
Pure Type ◽  
Reduction Property ◽  
Explicit Substitution ◽  
Pure Type Systems

We define an extension of pure type systems with explicit substitution. We show that the type systems with explicit substitution are strongly normalizing iff their ordinary counterparts are. Subject reduction is shown to fail in general but a weaker, though still useful, subject reduction property is established. A more complicated extension is proposed for which subject reduction does hold in general.

scholarly journals ON STEPWISE EXPLICIT SUBSTITUTION

1993 ◽  
Vol 04 (03) ◽  
pp. 197-240 ◽  
Author(s):  
FAIROUZ KAMAREDDINE ◽  
ROB NEDERPELT
Keyword(s):  
Lambda Calculus ◽  
Object Language ◽  
Explicit Substitution ◽  
Reduction Strategies ◽  
Partial Unfolding

This paper starts by setting the ground for a lambda calculus notation that strongly mirrors the two fundamental operations of term construction, namely abstraction and application. In particular, we single out those parts of a term, called items in the paper, that are added during abstraction and application. This item notation proves to be a powerful device for the representation of basic substitution steps, giving rise to different versions of β-reduction including local and global β-reduction. In other words substitution, thanks to the new notation, can be easily formalised as an object language notion rather than remaining a meta language one. Such formalisation will have advantages with respect to various areas including functional application and the partial unfolding of definitions. Moreover our substitution is, we believe, the most general to date. This is shown by the fact that our framework can accommodate most of the known reduction strategies, which range from local to global. Finally, we show how the calculus of substitution of Abadi et al., can be embedded into our calculus. We show moreover that many of the rules of Abadi et al. are easily derivable in our calculus.

Pure type systems with explicit substitutions

2015 ◽  
Vol 25 ◽  
Author(s):  
DANIEL FRIDLENDER ◽  
MIGUEL PAGANO
Keyword(s):  
Type Systems ◽  
Pure Type ◽  
Explicit Substitution ◽  
Explicit Substitutions ◽  
Pure Type Systems ◽  
De Bruijn ◽  
New Formulation ◽  
De Bruijn Indices ◽  
Meta Theory

AbstractWe introduce a new formulation of pure type systems (PTSs) with explicit substitution and de Bruijn indices and formally prove some of its meta-theory. Using techniques based on Normalisation by Evaluation, we prove that untyped conversion can be typed for predicative PTSs. Although this equivalence was settled by Siles and Herbelin for the conventional presentation of PTSs, we strongly conjecture that our proof method can also be applied to PTSs with η.

Functional runtime systems within the lambda-sigma calculus

1998 ◽  
Vol 8 (2) ◽  
pp. 131-176 ◽  
Author(s):  
THÉRÈSE HARDIN ◽  
LUC MARANGET ◽  
BRUNO PAGANO
Keyword(s):  
Runtime Systems ◽  
Formal Proofs ◽  
Input Language ◽  
Adequate Theory ◽  
Abstract Machines ◽  
Explicit Substitutions ◽  
Krivine Machine

We define a weak λ-calculus, λσw, as a subsystem of the full λ-calculus with explicit substitutions λσ[uArr ]. We claim that λσw could be the archetypal output language of functional compilers, just as the λ-calculus is their universal input language. Furthermore, λσ[uArr ] could be the adequate theory to establish the correctness of functional compilers. Here we illustrate these claims by proving the correctness of four simplified compilers and runtime systems modelled as abstract machines. The four machines we prove are the Krivine machine, the SECD, the FAM and the CAM. Thus, we give the first formal proofs of Cardelli's FAM and of its compiler.

Improving the lazy Krivine machine

2007 ◽  
Vol 20 (3) ◽  
pp. 271-293 ◽  
Author(s):  
Daniel P. Friedman ◽  
Abdulaziz Ghuloum ◽  
Jeremy G. Siek ◽  
Onnie Lynn Winebarger
Keyword(s):  
Krivine Machine

THE SOUNDNESS OF EXPLICIT SUBSTITUTION WITH NAMELESS VARIABLES

1998 ◽  
Vol 09 (03) ◽  
pp. 321-349
Author(s):  
FAIROUZ KAMAREDDINE
Keyword(s):  
Classical Calculus ◽  
Explicit Substitution ◽  
De Bruijn ◽  
De Bruijn Indices

We show the soundness of a λ-calculus ℬ where de Bruijn indices are used, substitution is explicit, and reduction is step-wise. This is done by interpreting ℬ in the classical calculus where the explicit substitution becomes implicit and de Bruijn indices become named variables. This is the first flat semantics of explicit substitution and step-wise reduction and the first clear account of exactly when α-reduction is needed.

scholarly journals Modeling, Sharing, and Recursion for Weak Reduction Strategies using Explicit Substitution

1996 ◽  
Vol 3 (56) ◽  
Author(s):  
Zine-El-Abidine Benaissa ◽  
Pierre Lescanne ◽  
Kristoffer H. Rose
Keyword(s):  
Programming Languages ◽  
Data Structures ◽  
Functional Programming ◽  
Explicit Substitution ◽  
Reduction Strategies ◽  
Recursive Data Structures ◽  
Recursive Data ◽  
Parallel Evaluation ◽  
Major Reduction ◽  
Weak Reduction

<p>We present the lambda sigma^a_w calculus, a formal synthesis of the concepts of<br />sharing and explicit substitution for weak reduction. We show how<br />lambda sigma^a_w can be used as a foundation of implementations of functional<br />programming languages by modelling the essential ingredients of such<br />implementations, namely weak reduction strategies, recursion, space<br />leaks, recursive data structures, and parallel evaluation, in a uniform way.<br />First, we give a precise account of the major reduction strategies<br />used in functional programming and the consequences of choosing <br /> lambda-graph-reduction vs. environment-based evaluation. Second, we show<br />how to add constructors and explicit recursion to give a precise account<br />of recursive functions and data structures even with respect to<br />space complexity. Third, we formalize the notion of space leaks in lambda sigma^a_w<br />and use this to define a space leak free calculus; this suggests optimisations<br />for call-by-need reduction that prevent space leaking and enables<br />us to prove that the "trimming" performed by the STG machine does<br />not leak space.<br />In summary we give a formal account of several implementation<br />techniques used by state of the art implementations of functional programming<br />languages.</p><p>Keywords. Implementation of functional programming, lambda<br />calculus, weak reduction, explicit substitution, sharing, recursion, space<br />leaks.</p>

scholarly journals Swapping: a natural bridge between named and indexed explicit substitution calculi

2011 ◽  
Vol 49 ◽  
pp. 1-15
Author(s):  
Ariel Mendelzon ◽  
Alejandro Ríos ◽  
Beta Ziliani
Keyword(s):  
Explicit Substitution

scholarly journals A Concrete Framework for Environment Machines

2006 ◽  
Vol 13 (3) ◽  
Author(s):  
Malgorzata Biernacka ◽  
Olivier Danvy
Keyword(s):  
Lambda Calculus ◽  
Intermediate Step ◽  
Abstract Machine ◽  
Abstract Machines ◽  
Reduction Strategies ◽  
Explicit Substitutions ◽  
One Step ◽  
The Common ◽  
Krivine Machine ◽  
Common Understanding

We materialize the common understanding that calculi with explicit substitutions provide an intermediate step between an abstract specification of substitution in the lambda-calculus and its concrete implementations. To this end, we go back to Curien's original calculus of closures (an early calculus with explicit substitutions), we extend it minimally so that it can also express one-step reduction strategies, and we methodically derive a series of environment machines from the specification of two one-step reduction strategies for the lambda-calculus: normal order and applicative order. The derivation extends Danvy and Nielsen's refocusing-based construction of abstract machines with two new steps: one for coalescing two successive transitions into one, and the other for unfolding a closure into a term and an environment in the resulting abstract machine. The resulting environment machines include both the Krivine machine and the original version of Krivine's machine, Felleisen et al.'s CEK machine, and Leroy's Zinc abstract machine.

Sign in / Sign up

Export Citation Format

Share Document