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. |
Papers
