S. Dans-un-modèle-classique,-comme-par-exemple-la-machine, )), et trois allerretours entre l'appelant et l'appelé se seraient produits. Le modèle d'exécution de Caml Light atteint donc presque la même efficacité que les techniques de décurryfication statique habituelles : les trois arguments de l'application curryfiée sont passés d'un seul coupàcoupà la fonction. (La seule perte d'efficacité est due aux tests sur le sommet de pile effectués par Grab.) Ce modèle se révèle plus puissant que la décurryfication statique dans le cas de fonctions curryfiées qui entremêlent passage d'arguments et calculs internes : let f = ?x

. Dans-cet-exemple, les trois arguments sont toujours passés en un seul coup, et on ne fait toujours qu'un aller-retour. Les techniques de décurryfication statique ne s'appliquent généralement pasàpasà des situations complexes comme celle-ci

. Le-modèle-d, exécution résumé ci-dessus sépare clairement suspension de l'´ evaluation (instruction Clos) et passage d'arguments (instruction Grab) Il permet donc la définition facile de suspensions, et par conséquent s'adapte

. Si-cette-variable-est-immédiatement-appliquée, ce qui est fréquent, on peut combiner en une seule application l'´ evaluation de la suspension avec l'application de la valeur de la suspension : CT (x r (a 1 ) . . . (a n )) = CN (a n ); Push; . . . ; CN (a 1 ); Push; Access(x r )

C. Appterm, = Pushmark; CN (a n ); Push; . . . ; CN (a 1 ); Push; Access(x r )

. En-conséquence, une fonction polymorphe s'effectue aussi efficacement en polymorphisme par nom qu'en polymorphisme par valeur Considérons le fragment de code typique : d'autres formalismes mathématiquement plus riches ; mais on y gagne des preuves accessibles et qui s'adaptent bienàbienà trois situations assez diverses. De même que la sémantique relationnelle se révèle très proche d'une exécution directe par machine

L. Méthodes-qui-m, enentàenentà ce résultat sont simples : introduire des indirections pour décrire par des termes finis des situations cycliques (´ etats mémoires, pour les références ; ensembles de contraintes, pour les types de fermetures) ; raisonner par récurrence structurelle sur les valeurs ; et considérer les fermetures et les continuations comme des expressions en attente, dont le typage sémantique se confond avec le typage syntaxique, et non pas comme des transformateurs de valeurs, dont le typage sémantique se fait par la condition de continuité. Ces techniques se trouvent pour la

. Ce-qui-estétonnantestétonnant,-c-'est-que-ce, théorème de non-communication " et l'opération de simplification des types de fermetures qu'il justifie n

H. A¨?ta¨?t-kaci and R. Nasr, Integrating logic and functional programming, Lisp and Symbolic Computation, pp.51-89, 1989.

A. W. Appel, Compiling with continuations, 1992.
DOI : 10.1017/CBO9780511609619

W. Andrew, D. B. Appel, and . Macqueen, Standard ML reference manual (preliminary)

L. Augustsson, A compiler for lazy ML, Proceedings of the 1984 ACM Symposium on LISP and functional programming , LFP '84, pp.218-227, 1984.
DOI : 10.1145/800055.802038

G. Henry and . Baker, Unify and conquer (garbage, updating, aliasing, . . . ) in functional languages, Lisp and Functional Programming, 1990.

J. Métayer, A new computational model and its discipline of programming, 1986.

D. Berry, The Edinburgh SML library Rapport technique ECS-LFCS-91-148, 1991.

D. Berry, R. Milner, and D. N. Turner, A semantics for ML concurrency primitives, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '92, pp.119-129, 1992.
DOI : 10.1145/143165.143191

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.36.7958

G. Berry and G. Boudol, The chemical abstract machine, 17th symposium Principles of Programming Languages, 1990.
DOI : 10.1145/96709.96717

URL : https://hal.archives-ouvertes.fr/inria-00075426

B. Berthomieu, L. Thierry, and . Sergent, Programming with behaviors in an ML framework ??? The syntax and semantics of LCS, Programming languages and systems ? ESOP '94, pp.89-104
DOI : 10.1007/3-540-57880-3_6

L. Cardelli, Basic polymorphic typechecking, Science of Computer Programming, vol.8, issue.2, pp.147-172, 1987.
DOI : 10.1016/0167-6423(87)90019-0

URL : http://doi.org/10.1016/0167-6423(87)90019-0

L. Cardelli, Typeful programming (rédacteurs), Formal description of programming concepts, pp.431-507, 1989.

L. Cardelli and J. C. Mitchell, Operations on records, Mathematical Foundations of Programming Semantics, pp.22-52, 1989.
DOI : 10.1007/BFb0040253

L. Cardelli and P. Wegner, On understanding types, data abstraction, and polymorphism. Computing surveys, pp.471-522, 1985.
DOI : 10.1145/6041.6042

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.117.695

N. Carriero and D. Gelerntner, Linda in context, Communications of the ACM, vol.32, issue.4, pp.444-458, 1989.
DOI : 10.1145/63334.63337

D. Clément, J. Despeyroux, T. Despeyroux, L. Hascoet, and G. Kahn, Natural semantics on the computer, 1985.

D. Clément, J. Despeyroux, T. Despeyroux, and G. Kahn, A simple applicative language: mini-ML, Proceedings of the 1986 ACM conference on LISP and functional programming , LFP '86, 1986.
DOI : 10.1145/319838.319847

G. Cousineau, P. Curien, and M. Mauny, The categorical abstract machine, Science of Computer Programming, vol.8, issue.2, pp.173-202, 1987.
DOI : 10.1016/0167-6423(87)90020-7

URL : http://dx.doi.org/10.1016/0167-6423(87)90020-7

G. Cousineau and G. Huet, The CAML primer. Rapport technique 122, 1990.
URL : https://hal.archives-ouvertes.fr/inria-00070045

P. Cousot and R. Cousot, Inductive definitions, semantics and abstract interpretations, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '92, pp.83-94, 1992.
DOI : 10.1145/143165.143184

L. Damas, Type assignment in programming languages, Thèse de PhD, 1985.

L. Damas and R. Milner, Principal type-schemes for functional programs, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '82, pp.207-212, 1982.
DOI : 10.1145/582153.582176

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.645.5233

R. Daniel-de, An implementation of monomorphic dynamics in ML using closures and references, 1991.

G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Paulin-mohring et al., The Coq proof assistant user's guide: version 5.6, 1991.

F. Bruce, R. Duba, D. B. Harper, and . Macqueen, Typing first-class continuations in ML, 18th symposium Principles of Programming Languages, pp.163-173, 1991.

M. Felleisen, P. Daniel, and . Friedman, A syntactic theory of sequential state, Theoretical Computer Science, vol.69, issue.3, pp.243-287, 1989.
DOI : 10.1016/0304-3975(89)90069-8

M. Felleisen, D. P. Friedman, E. Kohlbecker, and B. Duba, A syntactic theory of sequential control, Theoretical Computer Science, vol.52, issue.3, pp.205-237, 1987.
DOI : 10.1016/0304-3975(87)90109-5

Y. Fuh and P. Mishra, Type inference with subtypes, Lecture Notes in Computer Science, vol.88, issue.300, pp.94-114, 1988.

K. David, J. M. Gifford, and . Lucassen, Integrating functional and imperative programming, 13th symposium Principles of Programming Languages, pp.28-38, 1986.

J. Girard, Interprétation fonctionnelle etéliminationetélimination des coupures de l'arithmétique d'ordre supérieur, Thèse d' ´ Etat, 1972.

A. Carl, D. Gunter, and . Rémy, Ravl: A language for programming with records and variants. SoumisàSoumisà publication, 1992.

A. Carl, D. S. Gunter, and . Scott, Semantic domains, pp.635-674

R. Harper, Introduction to Standard ML. Rapport technique ECS-LFCS-86-14, 1986.

R. Harper and M. Lillibridge, ML with callcc is unsound. Message de la liste de distribution sml, 1991.

C. T. Haynes, D. P. Friedman, and M. Wand, Obtaining coroutines with continuations, Computer Languages, vol.11, issue.3-4, pp.143-153, 1986.
DOI : 10.1016/0096-0551(86)90007-X

C. A. Hoare, Communicating sequential processes, 1985.
DOI : 10.1007/978-1-4757-3472-0_16

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.132.6772

A. Lalita, J. C. Jategaonkar, and . Mitchell, ML with extended pattern matching and subtypes, Lisp and Functional Programming, pp.198-211, 1988.

P. Jouvelot and D. K. Gifford, Algebraic reconstruction of types and effects, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '91, pp.303-310, 1991.
DOI : 10.1145/99583.99623

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.9389

G. Kahn, The semantics of a simple language for parallel programming, Information processing 74, pp.471-475, 1974.

G. Kahn, Natural semantics, Programming of Future Generation Computers, pp.237-257, 1988.
DOI : 10.1007/BFb0039592

URL : https://hal.archives-ouvertes.fr/inria-00075953

G. Kahn and D. B. Macqueen, Coroutines and networks of parallel processes, 1976.
URL : https://hal.archives-ouvertes.fr/inria-00306565

P. Kanellakis and J. C. Mitchell, Polymorphic unification and ML typing, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '89, 1989.
DOI : 10.1145/75277.75286

Y. Lafont, Interaction nets, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '90, 1990.
DOI : 10.1145/96709.96718

P. J. Landin, The Mechanical Evaluation of Expressions, The Computer Journal, vol.6, issue.4, pp.308-320, 1964.
DOI : 10.1093/comjnl/6.4.308

P. J. Landin, The next 700 programming languages, Communications of the ACM, vol.9, issue.3, pp.157-165, 1966.
DOI : 10.1145/365230.365257

X. Leroy, Une extension de Caml vers la programmation logique. Mémoire depremì ere année, 1988.

X. Leroy, The ZINC experiment: an economical implementation of the ML language, 1990.
URL : https://hal.archives-ouvertes.fr/inria-00070049

X. Leroy, Unboxed objects and polymorphic typing, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '92, pp.177-188, 1992.
DOI : 10.1145/143165.143205

URL : https://hal.archives-ouvertes.fr/hal-01499973

X. Leroy and P. Weis, Polymorphic type inference and assignment, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '91, pp.291-302, 1991.
DOI : 10.1145/99583.99622

URL : https://hal.archives-ouvertes.fr/hal-01499974

B. Liskov, R. Atkinson, and T. Bloom, CLU reference manual, Lecture Notes in Computer Science, vol.114, 1981.

M. John, D. K. Lucassen, and . Gifford, Polymorphic effect systems, 15th symposium Principles of Programming Languages, pp.47-57, 1988.

D. B. Macqueen, Modules for standard ML, Proceedings of the 1984 ACM Symposium on LISP and functional programming , LFP '84, 1986.
DOI : 10.1145/800055.802036

D. B. Macqueen, G. Plotkin, and R. Sethi, An ideal model for recursive polymorphic types, Information and Control, vol.71, issue.1-2, pp.95-130, 1986.
DOI : 10.1016/S0019-9958(86)80019-5

C. J. David and . Matthews, Poly manual. Rapport technique 63, 1985.

M. Mauny, Functional programming using Caml Light. INRIA, 1991

R. Milner, A theory of type polymorphism in programming, Journal of Computer and System Sciences, vol.17, issue.3, pp.348-375, 1978.
DOI : 10.1016/0022-0000(78)90014-4

R. Milner, Communication and Concurrency, 1990.

R. Milner, Message de la liste de distribution sml, 1991.

R. Milner, J. Parrow, and D. Walker, A calculus of mobile processes: part 1. Rapport de recherche ECS-LFCS-89-85, 1989.

R. Milner and M. Tofte, Co-induction in relational semantics, Theoretical Computer Science, vol.87, issue.1, pp.209-220, 1991.
DOI : 10.1016/0304-3975(91)90033-X

URL : http://doi.org/10.1016/0304-3975(91)90033-x

R. Milner, M. Tofte, R. Harper, and D. Macqueen, The definition of Standard ML (revised), 1997.

C. John and . Mitchell, Coercion and type inference, 11th symposium Principles of Programming Languages, pp.175-185, 1984.

C. John and . Mitchell, Type systems for programming languages, pp.367-458

V. Nabokov, Ada or ardor, a family chronicle, 1969.

F. Nielson, The typed ??-calculus with first-class processes, PARLE '89, pp.357-373, 1989.
DOI : 10.1007/3-540-51285-3_52

A. Ohori and P. Buneman, Type inference in a database language, Lisp and Functional Programming, pp.174-183, 1988.
DOI : 10.1145/62678.62700

L. David and . Parnas, On the criteria to be used in decomposing systems into modules, Communications of the ACM, vol.15, issue.12, pp.1053-1058, 1972.

C. Lawrence and . Paulson, ML for the working programmer, 1991.

L. Simon and -. Peyton, The implementation of functional programming languages, 1987.

G. D. Plotkin, A structural approach to operational semantics, Journal of Logic and Algebraic Programming, pp.60-6117, 2004.

V. Poirriez, Intégration de fonctionnalités logiques dans un langage fonctionnel fortement typé: MLOG, une extension de ML, Thèse de doctorat, 1991.

J. A. Rees and W. Clinger, Revised report on the algorithmic language scheme, ACM SIGPLAN Notices, vol.21, issue.12, 1986.
DOI : 10.1145/15042.15043

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.111.6137

D. Rémy, Records and variants as a natural extension of ML, 16th symposium Principles of Programming Languages, pp.77-88, 1989.

D. Rémy, Algèbres touffues Application au typage polymorphe des objets enregistrements dans les langages fonctionnels, Thèse de doctorat, 1991.

D. Rémy, Type inference for records in a natural extension of ML (rédacteurs), Theoretical Aspects of Object-Oriented Programming, 1993.

J. H. Reppy, First-class synchronous operations in Standard ML, 1989.
DOI : 10.1007/bfb0026573

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.50.4202

J. H. Reppy, CML: a higher-order concurrent language, SIGPLAN Notices, vol.6, issue.26, pp.293-305, 1991.

C. John and . Reynolds, Toward a theory of type structure, Programming Symposium, pp.408-425, 1974.

C. John and . Reynolds, Three approaches to type structure, Mathematical Foundations of Software Development (TAPSOFT 85), pp.97-138, 1985.

C. John and . Reynolds, Preliminary design of the programming language Forsythe. Rapport technique CMU-CS-88-159, 1988.

J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM, vol.12, issue.1, pp.23-41, 1965.
DOI : 10.1145/321250.321253

F. Rouaix, ALCOOL-90: Typage de la surcharge dans un langage fonctionnel, Thèse de doctorat, 1990.

F. Rouaix, Safe run-time overloading, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '90, 1990.
DOI : 10.1145/96709.96746

G. Smolka, FRESH: a higher-order language with unification and multiple results, Logic Programming: Functions, Relations, and Equations, pp.469-524, 1986.

J. Talpin and P. Jouvelot, The type and effect discipline, Logic in Computer Science, 1992.
DOI : 10.1109/lics.1992.185530

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.54.5309

B. Thomsen, A calculus of higher-order communicationg systems, 16th symposium Principles of Programming Languages, 1989.

M. Tofte, Operational semantics and polymorphic type inference, Thèse de PhD CST-52- 88, 1988.

M. Tofte, Type inference for polymorphic references. Information and Computation, 1990.
DOI : 10.1016/0890-5401(90)90018-d

URL : http://doi.org/10.1016/0890-5401(90)90018-d

A. David and . Turner, Miranda, a non-strict functional language with polymorphic types, In Functional Programming Languages and Computer Architecture Lecture Notes in Computer Science, vol.201, pp.1-16, 1985.

J. Van-leeuwen, Handbook of Theoretical Computer Science, volume B, 1990.

M. Wand, Continuation-based multiprocessing, Proceedings of the 1980 ACM conference on LISP and functional programming , LFP '80, pp.19-28, 1980.
DOI : 10.1145/800087.802786

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.44.5351

M. Wand, Complete type inference for simple objects, Logic in Computer Science, pp.37-44, 1987.
DOI : 10.1109/lics.1988.5111

P. Weis, The CAML reference manual, version 2.6.1. Rapport technique 121, 1990.

K. Andrew and . Wright, Typing references by effect inference, European Symposium on Programming, 1992.

K. Andrew, M. Wright, and . Felleisen, A syntactic approach to type soundness, Information and Computation, vol.115, issue.1, pp.38-94, 1994.

.. Comparaison-avec-d-'autres-systèmes, 137 5.2.1 Les variables faibles, p.142

.. Présentation-informelle, 153 6.1.1 Les sémantiques du polymorphisme, p.155

.. Sémantique-opérationnelle, 157 6.2.1 Cas des références, Cas des continuations, p.160

S. Preuves-de, 160 6.3.1 Cas des références, Cas des continuations, p.165