, « The Calculus of Constructions, COQUAND (Thierry) & HUET (Gérard), vol.76, pp.95-120
, Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur
, Handbook of Logic in Computer Science, Computational Structures), vol.2, pp.117-309
, 17th ACM Symposium on Principles of Programming Languages, pp.31-46
, « From ?? to ?v: a journey through calculi of explicit substitutions, 21st ACM Symposium on Principles of Programming Languages, pp.60-69
, Kristoffer Høgsbro), « Preservation of strong normalisation in named lambda-calculi with explicit substitution and garbage collection, pp.62-72
, LESCANNE (Pierre), « Reduction, intersection types and explicit substitutions, Mathematical Structures in Computer Science, vol.13, issue.1, pp.55-85
, « Cut rules and explicit substitutions, Mathematical Structures in Computer Science, vol.11, issue.1, pp.131-168
, « Pure type systems with explicit substitution, BLOO (Roel), vol.11, pp.3-19
, « Intersection types for explicit substitutions ». Information and Computation, vol.189, pp.17-42
, « Strong normalization of explicit substitutions via cut elimination in proof nets, pp.35-46
, KESNER (Delia) & POLONOVSKI (Emmanuel), « Proof nets and explicit substitutions, Mathematical Structures in Computer Science, vol.13, issue.3, pp.409-450
, « Explicit substitutions and reducibility, vol.11, pp.29-449
, « Dependent types and explicit substitutions, Mathematical Structures in Computer Science, vol.11, issue.1, pp.91-129
, Preservation of Termination for Explicit Substitution, BLOO
, LAFONT (Yves) & TAYLOR (Paul), Proofs and Types
, « Substitutions explicites dans le ?-cube ». Mémoire de DÉA, École normale supérieure de Lyon, juillet ????
, BARENDREGT (Hendrik), Lambda-calculus, its Syntax and its Semantics. Coll. « Studies in Logic and the Foundation of Mathematics
, Lambda-calcul, types et modèles. Coll. « Études et recherches en informatique