Denotational aspects of untyped normalization by evaluation
Andrzej Filinski; Henning Korsholm Rohde
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications (2005)
- Volume: 39, Issue: 3, page 423-453
- ISSN: 0988-3754
Access Full Article
topAbstract
topHow to cite
topReferences
top- [1] K. Aehlig and F. Joachimski, Operational aspects of untyped normalization by evaluation. Math. Structures Comput. Sci. 14 (2004) 587–611. Zbl1090.68018
- [2] H.P. Barendregt, The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, revised edition (1984). Zbl0551.03007MR774952
- [3] U. Berger and H. Schwichtenberg, An inverse of the evaluation functional for typed -calculus, in Proc. of the Sixth Annual IEEE Symposium on Logic in Computer Science, Amsterdam, The Netherlands (July 1991) 203–211.
- [4] T. Coquand and P. Dybjer, Intuitionistic model constructions and normalization proofs. Math. Structures Comput. Sci. 7 (1997) 75–94. Zbl0883.03009
- [5] A. Filinski, 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 Zbl0953.68034
- [6] A. Filinski and H.K. Rohde, 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. Zbl1126.68335
- [7] A. Filinski and H.K. Rohde, 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/. Zbl1096.03010
- [8] B. Grégoire and X. Leroy, 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. Zbl1322.68053
- [9] R. Milner, M. Tofte, R. Harper and D. MacQueen, The Definition of Standard ML. The MIT Press, revised edition (1997).
- [10] J.C. Mitchell, Foundations for Programming Languages. The MIT Press (1996).
- [11] A.M. Pitts, Computational adequacy via “mixed” inductive definitions, in Mathematical Foundations of Programming Semantics. Springer-Verlag. Lect. Notes Comput. Sci. 802 (1993) 72–82.
- [12] A.M. Pitts, Relational properties of domains. Inform. Comput. 127 (1996) 66–90. Zbl0868.68037
- [13] G.D. Plotkin, LCF considered as a programming language. Theor. Comput. Sci. 5 (1977) 223–255. Zbl0369.68006
- [14] M.R. Shinwell, A.M. Pitts and M.J. Gabbay, FreshML: Programming with binders made simple, in Eighth ACM SIGPLAN International Conference on Functional Programming, ACM Press, Uppsala, Sweden (2003) 263–274. Zbl1315.68058