The bologna optimal higher-order machine

Journal of Functional Programming - Tập 6 Số 6 - Trang 763-810 - 1996
Andrea Asperti1, Cecilia Giovannetti1, Andrea Naletto1
1Dipartimento di Matematica, P.zza di Porta S.Donato 5, Bologna, Italy (

Tóm tắt

AbstractThe Bologna Optimal Higher-order Machine (BOHM) is a prototype implementation of the core of a functional language based on (a variant of) Lamping's optimal graph reduction technique (Lamping, 1990; Gonthier et al., 1992a; Asperti, 1994). The source language is a sugared λ-calculus enriched with booleans, integers, lists and basic operations on these data types (following the guidelines of Interaction Systems – Asperti and Laneve (1993b, 1994), Laneve (1993)). In this paper, we shall describe BOHM's general architecture (comprising the garbage collector), and give a large set of benchmarks and experimental results.

Từ khóa


Tài liệu tham khảo

Leroy, 1992, The Caml Light system, release 0.5. Documentation and user's manual

Aczel P. (1978) A general Church–Rosser Theorem. Draft, Manchester.

Lévy, 1978, Thèse de doctorat d'état

Asperti, 1994, Proc. LICS'94

Asperti, 1995, Proc. 2nd International Conference on Typed Lambda Calculi and Applications – TLCA'95

Gonthier G. , Abadi M. and Lévy J. J. (1992a) The geometry of optimal lambda reduction. Proc. 19th Symposium on Principles of Programming Languages – POPL 92.

Danos V. and Regnier L. (1993) Local and asynchronous beta-reduction. Proc. 8th Annual Symposium on Logic in Computer Science – LICS 93, Montreal.

Asperti, 1993, Technical Report UBLCS-93-12

Girard J. Y. Geometry of interaction II: Deadlock-free algorithms. Proc. International Conference on Computer Logic – COLOG 88.Springer-Verlag.

Lévy, 1980, To H. B.Curry, Essays on Combinatory Logic, Lambda Calculus and Formalism, 159

Asperti A. and Laneve C. (1994) Interaction Systems I: the theory of optimal reductions. Mathematical Structures in Computer Science.

Wadsworth C. P. (1971) Semantics and pragmatics of the λ-calculus. PhD thesis, Oxford University.

Girard, 1989, Proofs and Types

Lamping, 1990, Proc. 17th Symposium on Principles of Programming Languages – POPL 90

Asperti, 1995, Proc. Sixth International Conference on Rewriting Techniques and Applications – RTA'95

Naletto, 1994, Dissertazione di Laurea

Asperti, 1994, Fundamenta Informaticae

Girard, 1986, Linear logic, Theoretical Computer Science, 50

Asperti, 1993, Theoretical Computer Science

Lamping J. (1989) An algorithm for optimal lambda calculus reductions. Xerox PARC Internal Report.

Lafont, 1990, Proc. 17th Symposium on Principles of Programming Languages – POPL 90

Field J. (1990) On laziness and optimality in lambda interpreters: tools for specification and analysis. Proc. 17th ACM Symposium on Principles of Programmining Languages – POPL 90.

Giovannetti, 1994, Dissertazione di Laurea

Peyton Jones, 1987, The Implementation of Functional Programming Languages

Klop J. W. (1980) Combinatory reduction system. PhD Thesis, Mathematisch Centrum, Amsterdam.

Laneve C. (1993) Optimality and concurrency in interaction systems. PhD thesis, Dip. Informatica, Università di Pisa.

Regnier, 1992, Thèse de doctorat

Girard, 1988, Logic Colloquium '88

Gonthier G. , Abadi M. and Lévy J. J. (1992b) Linear logic without boxes. Proc. 7th Annual Symposium on Logic in Computer Science – LICS'92.

Thông tin
Thông tin xuất bản

Journal of Functional Programming

Tập 6 Số 6

763-810

Thông tin tác giả