While Loops in Coq

Nowak, David; Rusu, Vlad

Type de document :

Communication dans un congrès avec actes

DOI :

10.4204/eptcs.389.8

Titre :

While Loops in Coq

Auteur(s) :

Nowak, David [Auteur]

Centre National de la Recherche Scientifique [CNRS]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Extra Small Extra Safe [2XS]
Rusu, Vlad [Auteur]

Analyse symbolique et conception orientée composants pour des systèmes embarqués temps-réel modulaires [SYCOMORES]

Titre de la manifestation scientifique :

7th Symposium on Working Formal Methods (FROM 2023)

Ville :

Bucarest

Pays :

Roumanie

Date de début de la manifestation scientifique :

2023-09-21

Titre de l’ouvrage :

Electronic Proceedings in Theoretical Computer Science

Date de publication :

2023-09-22

Mot(s)-clé(s) en anglais :

partial recursive functions
while loops -
Coq proof assistant

Discipline(s) HAL :

Informatique [cs]/Logique en informatique [cs.LO]

Résumé en anglais : [en]

While loops are present in virtually all imperative programming languages. They are important both for practical reasons (performing a number of iterations not known in advance) and theoretical reasons (achieving Turing ...
Lire la suite >While loops are present in virtually all imperative programming languages. They are important both for practical reasons (performing a number of iterations not known in advance) and theoretical reasons (achieving Turing completeness). In this paper we propose an approach for incorporating while loops in an imperative language shallowly embedded in the Coq proof assistant. The main difficulty is that proving the termination of while loops is nontrivial, or impossible in the case of nontermination, whereas Coq only accepts programs endowed with termination proofs. Our solution is based on a new, general method for defining possibly non-terminating recursive functions in Coq. We illustrate the approach by proving termination and partial correctness of a program on linked lists.Lire moins >

Langue :

Anglais

Comité de lecture :

Oui

Audience :

Internationale

Vulgarisation :

Non

Collections :

Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189

Source :

Harvested from HAL

Fichiers

document
Accès libre
Accéder au document

paper.pdf
Accès libre
Accéder au document

document
Accès libre
Accéder au document

paper.pdf
Accès libre
Accéder au document

While Loops in Coq BibTeX CSV Excel RIS

Fichiers

While Loops in Coq

BibTeX

CSV

Excel

RIS