Skip to Main content Skip to Navigation

Certified reasoning on real numbers and objects in co-inductive type theory

Abstract : We adopt Formal Methods based on Type Theory for reasoning on the semantics of computer programs: the ultimate goal is to prove that a fragment of software meets its formal specification. Application areas of our research are the Real Numbers datatype and the Object-oriented Languages based on Objects. In the first part we construct the Real Numbers using streams, i.e. infinite sequences, of signed digits. We implement the Reals in Coq using streams, which are managed using coinductive judgments and corecursive algorithms. Then we introduce a constructive axiomatization and we use it for proving the adequacy of our construction. In the second part we approach Object-based Calculi with side-effects, focusing on Abadi and Cardelli's imp[sigma]. We reformulate imp[sigma] using modern encoding techniques, as Higher-Order Abstract Syntax and Coinductive proof systems in Natural Deduction style. Then we formalize imp[sigma] in Coq and we prove the Type Soundness.
Document type :
Complete list of metadata
Contributor : Thèses Ul <>
Submitted on : Thursday, March 29, 2018 - 12:40:20 PM
Last modification on : Tuesday, April 24, 2018 - 1:30:13 PM


Files produced by the author(s)


  • HAL Id : tel-01750193, version 1



Alberto Ciaffaglione. Certified reasoning on real numbers and objects in co-inductive type theory. Autre [cs.OH]. Institut National Polytechnique de Lorraine, 2003. Français. ⟨NNT : 2003INPL026N⟩. ⟨tel-01750193⟩



Record views


Files downloads