Law can be shown to be inhabited in ?µ?µ?µ?µ by the term ?z.µ?.z|(?y.µ?.y|?) · ? [14] which is itself the reduction of the translation of the ?µ-term given by Ong and ,
Explicit substitutions, Journal of Functional Programming, vol.1, issue.4, pp.375-416, 1991. ,
URL : https://hal.archives-ouvertes.fr/inria-00075382
, Compilers: Principles, Techniques and Tools, 1988.
Continuation-passing, closure-passing style, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp.293-302, 1989. ,
A symmetric lambda calculus for classical program extraction, Information and Computation, vol.125, issue.2, pp.103-117, 1996. ,
The Lambda Calculus: its Syntax and Semantics, 1984. ,
Lambda terms for natural deduction, sequent calculus and cut-elimination, Journal of Functional Porgramming, vol.10, issue.1, pp.121-134, 2000. ,
Preservation of strong normalisation in named lambda calculi with explicit substitution and garbage collection, CSN'95 -Computer Science in the Netherlands, pp.62-72, 1995. ,
An overview of elan, Proceedings of the 2nd International Workshop on Rewriting Logic and its Applications, 1998. ,
URL : https://hal.archives-ouvertes.fr/inria-00098518
The maude 2.0 system, Rewriting Techniques and Applications (RTA 2003), number 2706 in Lecture Notes in Computer Science, pp.76-87, 2003. ,
The duality of computation, Proceedings of the 5 th ACM SIGPLAN International Conference on Functional Programming (ICFP'00), pp.233-243, 2000. ,
URL : https://hal.archives-ouvertes.fr/inria-00156377
Computational isomorphisms in classical logic (extended abstract), Electronic Notes in Theoretical Computer Science, vol.3, 1996. ,
A new deconstructive logic: Linear logic, The Journal of Symbolic Logic, vol.62, 1997. ,
, Mathematical Intuitionism: Introduction to Proof Theory, 1987.
Classical proofs, typed processes and intersection types, TYPES'03, 2004. ,
Linear logic, Theoretical Computer Science, vol.50, pp.1-102, 1987. ,
URL : https://hal.archives-ouvertes.fr/inria-00075966
A new constructive logic: classical logic, Mathematical Structures in Computer Science, vol.1, issue.3, pp.255-296, 1991. ,
URL : https://hal.archives-ouvertes.fr/inria-00075117
Séquents qu'on calcule : de l'interprétation du calcul des séquents comme calcul de ?-termes et comme calcul de stratégies gagnantes, 1995. ,
Computer simulation of peptide interaction with an rp-hplc sorbent, J.Phys.Chem.B, vol.101, pp.10962-10970, 1997. ,
Call-by-value, call-by-name, and strong normalization for the classical sequent calculus, Electronic Notes in Theoretical Computer Science, vol.86, 2003. ,
URL : https://hal.archives-ouvertes.fr/hal-00150290
Intersection types for explicit substitutions, Information and Computation, vol.189, issue.1, pp.17-42, 2004. ,
URL : https://hal.archives-ouvertes.fr/hal-00150285
From ?? to ??, a journey through calculi of explicit substitutions, Proceedings of the 21st Annual ACM Symposium on Principles Of Programming Languages, pp.60-69, 1994. ,
Communicating and mobile systems: the ?-calculus, 1999. ,
A Curry-Howard foundation for functional computation with control, Proceedings of the 24th Annual ACM Symposium on Principles Of Programming Languages, pp.215-227, 1997. ,
An algorithmic interpretation of classical natural deduction, Proc. of Int. Conf. on Logic Programming and Automated Reasoning, LPAR'92, pp.190-201, 1992. ,
Classical Logic and Computation, 2000. ,
Term graphs, ?-conversion, and principal types for X ,
Call-by-Value is Dual to Call-by-Name, Proceedings of the eighth ACM SIGPLAN international conference on Functional programming, pp.189-201, 2003. ,
, , 1925.
, Principia Mathematica to *56. Cambridge Mathematical Library, 1997.