|
|
Logic & Semantics |
|
|
Logic & Semantics |
Dipartimento di Matematica e Informatica
Universita` di Udine
Udine - ITALY
(currently visiting LFCS - Edinburgh)
When using Higher Order Intuitionistic Type Theory as a Logical Framework, a very interesting possibility is that of using Higher Order Abstract Syntax (HOAS). HOAS, in fact, allows to express the syntax and the operational semantics of formal calculi involving operators on variables, names, and locations (e.g. binders, restriction ops., ``new name'' ops., assignments) in a uniform and algebraic way. HOAS is therefore extremely valuable both as a formalism for capturing certain context sensitive aspects of syntax and operational semantics, and for setting a standard on how alpha conversion should be handled in formal systems. However, even in powerful Logical Frameworks such as COQ, metatheoretic reasoning on HOAS is limited.
We illustrate benefits of HOAS as well as its drawbacks, and a possible axiomatic solution to them, using Milner's pi-calculus as a running example. In particular, we provide a final semantics for the pi-calculus [HLMP] and we present a large case study on the development of the elementary metatheory of strong late bisimilarity in COQ [HMS].
If time permits we discuss other issues arising in using Higher Order Intuitionistic Type Theory as a Logical Framework.
[HLMP] F. Honsell, M. Lenisa, U. Montanari, and M. Pistore. ``Final Semantics for the pi-calculus'', Programming Concepts and Methods PROCOMET'98, D. Gries et al. eds., Chapman & Hall, 1998. http://www.dimi.uniud.it/~lenisa/Papers/Compressed-ps/procomet98.ps.gz
[MMS] F. Honsell, M. Miculan, I. Scagnetto. ``pi-calculus in (Co)Inductive Type Theory'' to appear in TCS ftp://ftp.dimi.uniud.it/pub/miculan/TCS99.dvi.gz
