Skip to Main content Skip to Navigation

From types to logical assertions : automatic or assisted proofs of property about functional programs

Yann Régis-Gianas 1
1 PI.R2 - Design, study and implementation of languages for proofs and programs
PPS - Preuves, Programmes et Systèmes, Inria Paris-Rocquencourt, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique : UMR7126
Abstract : This work studies two approaches to improve the safety of computer programs using static analysis. The first one is typing which guarantees that the evaluation of program cannot fail. The functional language ML has a very rich type system and also an algorithm that infers automatically the types. We focus on its adaptation to generalized algebraic data types (GADTs). In this setting, efficient computation of a most general type is impossible. We propose a stratification of the language that retain the usual characteristics of the ML fragment and make explicit the use of GADTs. The re- sulting language, MLGX, entails a burden on the programmer who must annotate its programs too much. A second stratum, MLGI, offers a mechanism to infer locally, in a predictable and efficient way, incomplete yet, most of the type annotations. The first part concludes on an illustration of the expres- siveness of GADTs to encode the invariants of pushdown automata used in LR parsing. The second approach augments the language with logic assertions that enables arbitrarily complex specifications to be expressed. We check the compliance of the program semantics with respect to these specifica- tions thanks to a method called Hoare logic and thanks to semi-automatic computer-based proofs. The design choices permit to handle first-class functions. They are directed by an implementation which is illustrated by the certification of a module of trees that denote finite sets.
Document type :
Complete list of metadata

Cited literature [139 references]  Display  Hide  Download
Contributor : Yann Regis-Gianas Connect in order to contact the contributor
Submitted on : Sunday, December 6, 2015 - 9:19:37 PM
Last modification on : Friday, January 21, 2022 - 3:22:25 AM
Long-term archiving on: : Saturday, April 29, 2017 - 5:37:11 AM


  • HAL Id : tel-01238703, version 1



Yann Régis-Gianas. From types to logical assertions : automatic or assisted proofs of property about functional programs. Programming Languages [cs.PL]. Université paris diderot, 2007. English. ⟨NNT : 2007PA077155⟩. ⟨tel-01238703⟩



Record views


Files downloads