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 :
Theses
Complete list of metadatas

https://hal.univ-lorraine.fr/tel-01750193
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

File

INPL_T_2003_CIAFFAGLIONE_A.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : tel-01750193, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

28

Files downloads

55