We show that the standard normalization-by-evaluation construction for the simply-typed
Mots-clés : normalization by evaluation, untyped
@article{ITA_2005__39_3_423_0, author = {Filinski, Andrzej and Rohde, Henning Korsholm}, title = {Denotational aspects of untyped normalization by evaluation}, journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications}, pages = {423--453}, publisher = {EDP-Sciences}, volume = {39}, number = {3}, year = {2005}, doi = {10.1051/ita:2005026}, mrnumber = {2157044}, zbl = {1096.03010}, language = {en}, url = {https://www.numdam.org/articles/10.1051/ita:2005026/} }
TY - JOUR AU - Filinski, Andrzej AU - Rohde, Henning Korsholm TI - Denotational aspects of untyped normalization by evaluation JO - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications PY - 2005 SP - 423 EP - 453 VL - 39 IS - 3 PB - EDP-Sciences UR - https://www.numdam.org/articles/10.1051/ita:2005026/ DO - 10.1051/ita:2005026 LA - en ID - ITA_2005__39_3_423_0 ER -
%0 Journal Article %A Filinski, Andrzej %A Rohde, Henning Korsholm %T Denotational aspects of untyped normalization by evaluation %J RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications %D 2005 %P 423-453 %V 39 %N 3 %I EDP-Sciences %U https://www.numdam.org/articles/10.1051/ita:2005026/ %R 10.1051/ita:2005026 %G en %F ITA_2005__39_3_423_0
Filinski, Andrzej; Rohde, Henning Korsholm. Denotational aspects of untyped normalization by evaluation. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 39 (2005) no. 3, pp. 423-453. doi : 10.1051/ita:2005026. https://www.numdam.org/articles/10.1051/ita:2005026/
[1] Operational aspects of untyped normalization by evaluation. Math. Structures Comput. Sci. 14 (2004) 587-611. | Zbl
and ,[2] The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, revised edition (1984). | MR | Zbl
,
[3] An inverse of the evaluation functional for typed
[4] Intuitionistic model constructions and normalization proofs. Math. Structures Comput. Sci. 7 (1997) 75-94. | Zbl
and ,[5] A semantic account of type-directed partial evaluation, in International Conference on Principles and Practice of Declarative Programming, edited by G. Nadathur, Springer-Verlag, Paris, France. Lect. Notes Comput. Sci. 1702 (1999) 378-395 | Zbl
,[6] A denotational account of untyped normalization by evaluation, in 7th International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2004), edited by I. Walukiewicz, Springer-Verlag, Barcelona, Spain Lect. Notes Comput. Sci. 2987 (2004) 167-181. | Zbl
and ,[7] Denotational aspects of untyped normalization by evaluation (extended version, with detailed proofs). BRICS Report RS-05-4, University of Aarhus, Denmark (February 2005). Available from http://www.brics.dk/RS/05/4/.
and ,[8] A compiled implementation of strong reduction, in Proc. of the Seventh ACM SIGPLAN International Conference on Functional Programming, edited by S. Peyton Jones, ACM Press, Pittsburgh, Pennsylvania, SIGPLAN Notices 37 (2002) 235-246.
and ,[9] The Definition of Standard ML. The MIT Press, revised edition (1997).
, , and ,[10] Foundations for Programming Languages. The MIT Press (1996).
,[11] Computational adequacy via “mixed” inductive definitions, in Mathematical Foundations of Programming Semantics. Springer-Verlag. Lect. Notes Comput. Sci. 802 (1993) 72-82.
,[12] Relational properties of domains. Inform. Comput. 127 (1996) 66-90. | Zbl
,[13] LCF considered as a programming language. Theor. Comput. Sci. 5 (1977) 223-255. | Zbl
,[14] FreshML: Programming with binders made simple, in Eighth ACM SIGPLAN International Conference on Functional Programming, ACM Press, Uppsala, Sweden (2003) 263-274.
, and ,Cité par Sources :