### Skapa referens, olika format (klipp och klistra)

**Harvard**

Bove, A., Krauss, A. och Sozeau, M. (2016) *Partiality and recursion in interactive theorem provers – an overview*.

** BibTeX **

@conference{

Bove2016,

author={Bove, Ana and Krauss, Alexander and Sozeau, Matthieu},

title={Partiality and recursion in interactive theorem provers – an overview},

booktitle={Mathematical Structures in Computer Science},

pages={38-88},

abstract={The use of interactive theorem provers to establish the correctness of critical parts of a software development or for formalizing 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 several techniques that have been proposed in the literature to simplify the formalization 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.},

year={2016},

}

** RefWorks **

RT Conference Proceedings

SR Electronic

ID 210551

A1 Bove, Ana

A1 Krauss, Alexander

A1 Sozeau, Matthieu

T1 Partiality and recursion in interactive theorem provers – an overview

YR 2016

T2 Mathematical Structures in Computer Science

SP 38

OP 88

AB The use of interactive theorem provers to establish the correctness of critical parts of a software development or for formalizing 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 several techniques that have been proposed in the literature to simplify the formalization 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.

LA eng

DO 10.1017/S0960129514000115

LK http://dx.doi.org/10.1017/S0960129514000115

OL 30