Ivan Scagnetto

Reasoning about names in Higher-Order Abstract Syntax


The continuously growing application of computer science to a wide range of human activities yields several issues. Besides sociological, philosophical or other more or less arbitrary speculations, there is the pragmatic need of controlling the activity and predicting the behaviour of complex systems devoted to critical tasks or, more simply, to the accomplishment of online financial transactions. Most of the time, programmers convince themselves that their code meets the original specifications by informal arguments or by testing the software over some sample of input data. However, even at the dawn of the computer era, this approach has been considered unsatisfactory since it cannot ensure the absence of errors under all circumstances. On the other hand the formal methods of mathematics provide a rigorous way for reasoning and understanding the behaviour of programs, languages, and complex systems. Many logics and calculi have arisen in order to deal with a plethora of problems and properties. However, their application to real cases is often cumbersome and error prone due to the overwhelming complexity and the subtleties involved. The field of Computer Aided Formal Reasoning (CAFR) is a research branch whose aim is to study and implement tools allowing to develop formal proofs in a computer-assisted way. So doing, nothing can be "swept under the rug" (like it often happens with proofs carried out with "pencil and paper") and, once the proof is finished, its correctness is ensured, i.e., certified by the system. Recently Logical Frameworks (LFs) based on constructive type theory have emerged as general metalanguages for encoding and formally reasoning about formal systems by means of the propositions-as-types, proofs-as-terms paradigm. The latter allows to reduce the problem of proof checking to that of type checking opening the way to a mechanized implementation of LFs. The contribution of this thesis is the proposal of an axiomatic theory which, in conjunction with the Higher-Order Abstact Syntax (HOAS) encoding approach, allows to adequately encode and reason over a large class of formal systems. We hope that this work will help in the understanding and application of LFs.

Keywords: Formal Methods, Computer Aided Formal Reasoning; Logical Frameworks, Type Theory, Coq, Higher-Order Abstract Syntax; Functor Categories.


Download the thesis as a gzipped PDF file (901 KB).
Download the thesis as a gzipped PostScript file (657 KB).