-
Extracting Text from Proofs
In this paper, we propose a method for presenting formal proofs in an intelligible form. We describe a transducer from proof objects ($\lambda$-terms in the Calculus... -
QArith: Coq Formalisation of Lazy Rational Arithmetic
In this paper we present the formalisation of the library which is an implementation of rational numbers as binary sequences for both lazy and strict computation. We... -
Realizability and parametricity in Pure Type Systems
This thesis focuses on the adaptation of realizability and parametricity to dependent types in the framework of Pure Type Systems. We describe a systematic method to...
