Alberto Ciaffaglione
Certified reasoning on Real
Numbers and Objects in Co-inductive Type Theory
PhD thesis, Dipartimento di Matematica e Informatica Università di
Udine, Italy, 2003
available as outline
In the thesis we adopt Type Theory-based Formal
Methods, namely
the proof assistant Coq, for reasoning on two distinct topics.
In the first part we encode the Constructive Real Numbers in Coq using
infinite sequences of digits. Then we work on such a representation
with co-inductive types and co-recursive proofs. The final aim is to
prove in Coq that the representation satisfies a set of axioms,
proposed for characterizing the constructive reals.
In the second part we encode the Abadi-Cardelli's imp-varsigma
calculus in Coq using an higher-order approach. We formalize the
syntax, the first-order static semantics and the big-step dynamic
semantics. Then we prove a Subject Reduction theorem relating the
two semantics. The ultimate goal is to obtain a Type Soundness
result in Coq.
[ bib |
.pdf ]
Back
This file has been generated by
bibtex2html 1.43