Partiality and Recursion in Interactive Theorem Provers - An Overview

Ana Bove 1 Alexander Krauss 2 Matthieu Sozeau 3
3 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 : The use of interactive theorem provers to establish the correctness of critical parts of a software development or for formalising mathematics is becoming more common and feasible in practice. However, most mature theorem provers lack a direct treatment of partial and general recursive functions; overcoming this weakness has been the objective of intensive research during the last decades. In this article, we review many techniques that have been proposed in the literature to simplify the formalisation of partial and general recursive functions in interactive theorem provers. Moreover, we classify the techniques according to their theoretical basis and their practical use. This uniform presentation of the different techniques facilitates the comparison and highlights their commonalities and differences, as well as their relative advantages and limitations. We focus on theorem provers based on constructive type theory (in particular, Agda and Coq) and higher-order logic (in particular Isabelle/HOL). Other systems and logics are covered to a certain extent, but not exhaustively. In addition to the description of the techniques, we also demonstrate tools which facilitate working with the problematic functions in particular theorem provers.
Type de document :
Article dans une revue
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2012
Liste complète des métadonnées

Littérature citée [108 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00691459
Contributeur : Matthieu Sozeau <>
Soumis le : vendredi 26 octobre 2012 - 07:00:04
Dernière modification le : vendredi 25 mai 2018 - 12:02:06
Document(s) archivé(s) le : jeudi 15 décembre 2016 - 01:28:12

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00691459, version 1

Collections

INRIA | PPS | USPC

Citation

Ana Bove, Alexander Krauss, Matthieu Sozeau. Partiality and Recursion in Interactive Theorem Provers - An Overview. Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2012. 〈hal-00691459〉

Partager

Métriques

Consultations de la notice

393

Téléchargements de fichiers

242