)), 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 ,
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 ,
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 ,
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 ) ,
= Pushmark; CN (a n ); Push; . . . ; CN (a 1 ); Push; Access(x r ) ,
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 ,
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 ,
théorème de non-communication " et l'opération de simplification des types de fermetures qu'il justifie n ,
Integrating logic and functional programming, Lisp and Symbolic Computation, pp.51-89, 1989. ,
Compiling with continuations, 1992. ,
DOI : 10.1017/CBO9780511609619
Standard ML reference manual (preliminary) ,
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
Unify and conquer (garbage, updating, aliasing, . . . ) in functional languages, Lisp and Functional Programming, 1990. ,
A new computational model and its discipline of programming, 1986. ,
The Edinburgh SML library Rapport technique ECS-LFCS-91-148, 1991. ,
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
The chemical abstract machine, 17th symposium Principles of Programming Languages, 1990. ,
DOI : 10.1145/96709.96717
URL : https://hal.archives-ouvertes.fr/inria-00075426
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
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
Typeful programming (rédacteurs), Formal description of programming concepts, pp.431-507, 1989. ,
Operations on records, Mathematical Foundations of Programming Semantics, pp.22-52, 1989. ,
DOI : 10.1007/BFb0040253
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
Linda in context, Communications of the ACM, vol.32, issue.4, pp.444-458, 1989. ,
DOI : 10.1145/63334.63337
Natural semantics on the computer, 1985. ,
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
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
The CAML primer. Rapport technique 122, 1990. ,
URL : https://hal.archives-ouvertes.fr/inria-00070045
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
Type assignment in programming languages, Thèse de PhD, 1985. ,
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
An implementation of monomorphic dynamics in ML using closures and references, 1991. ,
The Coq proof assistant user's guide: version 5.6, 1991. ,
Typing first-class continuations in ML, 18th symposium Principles of Programming Languages, pp.163-173, 1991. ,
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
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
Type inference with subtypes, Lecture Notes in Computer Science, vol.88, issue.300, pp.94-114, 1988. ,
Integrating functional and imperative programming, 13th symposium Principles of Programming Languages, pp.28-38, 1986. ,
Interprétation fonctionnelle etéliminationetélimination des coupures de l'arithmétique d'ordre supérieur, Thèse d' ´ Etat, 1972. ,
Ravl: A language for programming with records and variants. SoumisàSoumisà publication, 1992. ,
Semantic domains, pp.635-674 ,
Introduction to Standard ML. Rapport technique ECS-LFCS-86-14, 1986. ,
ML with callcc is unsound. Message de la liste de distribution sml, 1991. ,
Obtaining coroutines with continuations, Computer Languages, vol.11, issue.3-4, pp.143-153, 1986. ,
DOI : 10.1016/0096-0551(86)90007-X
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
ML with extended pattern matching and subtypes, Lisp and Functional Programming, pp.198-211, 1988. ,
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
The semantics of a simple language for parallel programming, Information processing 74, pp.471-475, 1974. ,
Natural semantics, Programming of Future Generation Computers, pp.237-257, 1988. ,
DOI : 10.1007/BFb0039592
URL : https://hal.archives-ouvertes.fr/inria-00075953
Coroutines and networks of parallel processes, 1976. ,
URL : https://hal.archives-ouvertes.fr/inria-00306565
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
Interaction nets, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '90, 1990. ,
DOI : 10.1145/96709.96718
The Mechanical Evaluation of Expressions, The Computer Journal, vol.6, issue.4, pp.308-320, 1964. ,
DOI : 10.1093/comjnl/6.4.308
The next 700 programming languages, Communications of the ACM, vol.9, issue.3, pp.157-165, 1966. ,
DOI : 10.1145/365230.365257
Une extension de Caml vers la programmation logique. Mémoire depremì ere année, 1988. ,
The ZINC experiment: an economical implementation of the ML language, 1990. ,
URL : https://hal.archives-ouvertes.fr/inria-00070049
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
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
CLU reference manual, Lecture Notes in Computer Science, vol.114, 1981. ,
Polymorphic effect systems, 15th symposium Principles of Programming Languages, pp.47-57, 1988. ,
Modules for standard ML, Proceedings of the 1984 ACM Symposium on LISP and functional programming , LFP '84, 1986. ,
DOI : 10.1145/800055.802036
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
Poly manual. Rapport technique 63, 1985. ,
Functional programming using Caml Light. INRIA, 1991 ,
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
Communication and Concurrency, 1990. ,
Message de la liste de distribution sml, 1991. ,
A calculus of mobile processes: part 1. Rapport de recherche ECS-LFCS-89-85, 1989. ,
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
The definition of Standard ML (revised), 1997. ,
Coercion and type inference, 11th symposium Principles of Programming Languages, pp.175-185, 1984. ,
Type systems for programming languages, pp.367-458 ,
Ada or ardor, a family chronicle, 1969. ,
The typed ??-calculus with first-class processes, PARLE '89, pp.357-373, 1989. ,
DOI : 10.1007/3-540-51285-3_52
Type inference in a database language, Lisp and Functional Programming, pp.174-183, 1988. ,
DOI : 10.1145/62678.62700
On the criteria to be used in decomposing systems into modules, Communications of the ACM, vol.15, issue.12, pp.1053-1058, 1972. ,
ML for the working programmer, 1991. ,
The implementation of functional programming languages, 1987. ,
A structural approach to operational semantics, Journal of Logic and Algebraic Programming, pp.60-6117, 2004. ,
Intégration de fonctionnalités logiques dans un langage fonctionnel fortement typé: MLOG, une extension de ML, Thèse de doctorat, 1991. ,
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
Records and variants as a natural extension of ML, 16th symposium Principles of Programming Languages, pp.77-88, 1989. ,
Algèbres touffues Application au typage polymorphe des objets enregistrements dans les langages fonctionnels, Thèse de doctorat, 1991. ,
Type inference for records in a natural extension of ML (rédacteurs), Theoretical Aspects of Object-Oriented Programming, 1993. ,
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
CML: a higher-order concurrent language, SIGPLAN Notices, vol.6, issue.26, pp.293-305, 1991. ,
Toward a theory of type structure, Programming Symposium, pp.408-425, 1974. ,
Three approaches to type structure, Mathematical Foundations of Software Development (TAPSOFT 85), pp.97-138, 1985. ,
Preliminary design of the programming language Forsythe. Rapport technique CMU-CS-88-159, 1988. ,
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
ALCOOL-90: Typage de la surcharge dans un langage fonctionnel, Thèse de doctorat, 1990. ,
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
FRESH: a higher-order language with unification and multiple results, Logic Programming: Functions, Relations, and Equations, pp.469-524, 1986. ,
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
A calculus of higher-order communicationg systems, 16th symposium Principles of Programming Languages, 1989. ,
Operational semantics and polymorphic type inference, Thèse de PhD CST-52- 88, 1988. ,
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
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. ,
Handbook of Theoretical Computer Science, volume B, 1990. ,
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
Complete type inference for simple objects, Logic in Computer Science, pp.37-44, 1987. ,
DOI : 10.1109/lics.1988.5111
The CAML reference manual, version 2.6.1. Rapport technique 121, 1990. ,
Typing references by effect inference, European Symposium on Programming, 1992. ,
A syntactic approach to type soundness, Information and Computation, vol.115, issue.1, pp.38-94, 1994. ,
137 5.2.1 Les variables faibles, p.142 ,
153 6.1.1 Les sémantiques du polymorphisme, p.155 ,
157 6.2.1 Cas des références, Cas des continuations, p.160 ,
160 6.3.1 Cas des références, Cas des continuations, p.165 ,