Using Fields and Explicit Substitutions to Implement Objects and Functions in a de Bruijn Setting

1999 ◽  
pp. 204-219
Author(s):  
Eduardo Bonelli
Keyword(s):  
Explicit Substitutions ◽  
De Bruijn

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 η.

scholarly journals A λ-calculus with explicit weakening and explicit substitution

2001 ◽  
Vol 11 (1) ◽  
pp. 169-206 ◽  
Author(s):  
RENÉ DAVID ◽  
BRUNO GUILLAUME
Keyword(s):  
Strong Normalization ◽  
Explicit Substitution ◽  
Explicit Substitutions ◽  
De Bruijn ◽  
De Bruijn Indices

Since Melliès showed that λσ (a calculus of explicit substitutions) does not preserve the strong normalization of the β-reduction, it has become a challenge to find a calculus satisfying the following properties: step-by-step simulation of the β-reduction, confluence on terms with metavariables, strong normalization of the calculus of substitutions and preservation of the strong normalization of the λ-calculus. We present here such a calculus. The main novelty of this calculus (given with de Bruijn indices) is the use of labels that represent updating functions and correspond to explicit weakening. A typed version is also presented.

scholarly journals Proof nets and explicit substitutions

2003 ◽  
Vol 13 (3) ◽  
pp. 409-450 ◽  
Author(s):  
ROBERTO DI COSMO ◽  
DELIA KESNER ◽  
EMMANUEL POLONOVSKI
Keyword(s):  
Equivalence Relation ◽  
Simulation Technique ◽  
Cut Elimination ◽  
Complex Mechanism ◽  
Explicit Substitutions ◽  
Proof Nets ◽  
De Bruijn ◽  
The One ◽  
De Bruijn Indices

We refine the simulation technique introduced in Di Cosmo and Kesner (1997) to show strong normalisation of $\l$-calculi with explicit substitutions via termination of cut elimination in proof nets (Girard 1987). We first propose a notion of equivalence relation for proof nets that extends the one in Di Cosmo and Guerrini (1999), and show that cut elimination modulo this equivalence relation is terminating. We then show strong normalisation of the typed version of the $\ll$-calculus with de Bruijn indices (a calculus with full composition defined in David and Guillaume (1999)) using a translation from typed $\ll$ to proof nets. Finally, we propose a version of typed $\ll$ with named variables, which helps to give a better understanding of the complex mechanism of the explicit weakening notation introduced in the $\ll$-calculus with de Bruijn indices (David and Guillaume 1999).

scholarly journals Explicit Substitutions à la de Bruijn

2003 ◽  
Vol 85 (7) ◽  
pp. 86-105 ◽  
Author(s):  
Fairouz Kamareddine ◽  
Alejandro Ríos
Keyword(s):  
Explicit Substitutions ◽  
De Bruijn

λν, a calculus of explicit substitutions which preserves strong normalisation

1996 ◽  
Vol 6 (5) ◽  
pp. 699-722 ◽  
Author(s):  
Zine-El-Abidine Benaissa ◽  
Daniel Briaud ◽  
Pierre Lescanne ◽  
Jocelyne Rouyer-Degli
Keyword(s):  
Explicit Substitutions ◽  
De Bruijn

AbstractExplicit substitutions were proposed by Abadi, Cardelli, Curien, Hardin and Lévy to internalise substitutions into λ-calculus and to propose a mechanism for computing on substitutions. λν is another view of the same concept which aims to explain the process of substitution and to decompose it in small steps. It favours simplicity and preservation of strong normalisation. This way, another important property is missed, namely confluence on open terms. In spirit, λν is closely related to another calculus of explicit substitutions proposed by de Bruijn and called CλξΦ. In this paper, we introduce λν, we present CλξΦ in the same framework as λν and we compare both calculi. Moreover, we prove properties of λν; namely λν correctly implements β reduction, λν is confluent on closed terms, i.e. on terms of classical λ-calculus and on all terms that are derived from those terms, and finally λν preserves strong normalisation in the following sense: strongly β normalising terms are strongly λν normalising.

Sign in / Sign up

Export Citation Format

Share Document