zbMATH — the first resource for mathematics

Twelf and Delphin: logic and functional programming in a meta-logical framework. (English) Zbl 1122.68391
Kameyama, Yukiyoshi (ed.) et al., Functional and logic programming. 7th international symposium, FLOPS 2004, Nara, Japan, April 7–9, 2004. Proceedings. Berlin: Springer (ISBN 3-540-21402-X/pbk). Lecture Notes in Computer Science 2998, 22-23 (2004).
Summary: Logical framework research studies the design of meta-languages that support efficient encodings of object-languages and deductions prevalent in the areas of programming languages, mobile code and logics design. A meta-logical framework is a logical framework that, in addition, supports reasoning about these encodings. Over the previous decades various meta-logical frameworks have been developed and employed among them Nuprl, Isabelle, Coq, Lego, Maude, Elan and, of course, the meta-logical framework Twelf that is being discussed here. [F. Pfenning, “Logical frameworks”, in: A. Robinson (ed.) et al., Handbook of automated reasoning. In 2 vols. Amsterdam: North-Holland/Elsevier. 1063–1147 (2001; Zbl 0992.03038)] provides an excellent overview and a historical perspective of the field of logical frameworks. The fields of programming language design, safe and secure mobile code, verification of authorization and other security protocols and lately even experiment design in biology drive the development of the aforementioned frameworks and greatly benefit from their progress.
For the entire collection see [Zbl 1048.68005].
Reviewer: Reviewer (Berlin)
68N17 Logic programming
68N18 Functional programming and lambda calculus
Coq; Isabelle; LEGO; Maude; Nuprl; Twelf
Full Text: DOI