Formal Definitions and Proofs for Partial ...
Type de document :
Pré-publication ou Document de travail
Titre :
Formal Definitions and Proofs for Partial (Co)Recursive Functions
Auteur(s) :
Cheval, Horatiu [Auteur]
University of Bucharest [UniBuc]
Nowak, David [Auteur]
Extra Small Extra Safe [2XS]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Rusu, Vlad [Auteur]
Analyse symbolique et conception orientée composants pour des systèmes embarqués temps-réel modulaires [SYCOMORES]
University of Bucharest [UniBuc]
Nowak, David [Auteur]

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

Analyse symbolique et conception orientée composants pour des systèmes embarqués temps-réel modulaires [SYCOMORES]
Mot(s)-clé(s) en anglais :
partial (co)recursive functions
Coq proof assistant
Coq proof assistant
Discipline(s) HAL :
Informatique [cs]/Logique en informatique [cs.LO]
Résumé en anglais : [en]
Partial functions are a key concept in programming. Without partiality a programming language has limited expressiveness-it is not Turing-complete, hence, some programs cannot be written. In functional programming languages, ...
Lire la suite >Partial functions are a key concept in programming. Without partiality a programming language has limited expressiveness-it is not Turing-complete, hence, some programs cannot be written. In functional programming languages, partiality mostly originates from the non-termination of recursive functions. Corecursive functions are another source of partiality: here, the issue is not non-termination, but the inability to produce arbitrary large, finite approximations of a theoretically infinite output. Partial functions have been formally studied in the branch of theoretical computer science called domain theory. In this paper we propose to step up the level of formality by using the Coq proof assistant. The main difficulty is that Coq requires all functions to be total, since partiality would break the soundness of its underlying logic. We propose practical solutions for this issue, and others, which appear when one attempts to define and reason about partial (co)recursive functions in a total functional language.Lire moins >
Lire la suite >Partial functions are a key concept in programming. Without partiality a programming language has limited expressiveness-it is not Turing-complete, hence, some programs cannot be written. In functional programming languages, partiality mostly originates from the non-termination of recursive functions. Corecursive functions are another source of partiality: here, the issue is not non-termination, but the inability to produce arbitrary large, finite approximations of a theoretically infinite output. Partial functions have been formally studied in the branch of theoretical computer science called domain theory. In this paper we propose to step up the level of formality by using the Coq proof assistant. The main difficulty is that Coq requires all functions to be total, since partiality would break the soundness of its underlying logic. We propose practical solutions for this issue, and others, which appear when one attempts to define and reason about partial (co)recursive functions in a total functional language.Lire moins >
Langue :
Anglais
Projet Européen :
Collections :
Source :
Fichiers
- document
- Accès libre
- Accéder au document
- jlamp.pdf
- Accès libre
- Accéder au document