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

**Harvard**

Bove, A. (2003) *General Recursion in Type Theory*.

** BibTeX **

@conference{

Bove2003,

author={Bove, Ana},

title={General Recursion in Type Theory},

booktitle={Lecture Notes in Computer Science. International Workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24–28, 2002},

isbn={978-3-540-14031-3},

pages={39-58},

abstract={In this work, a method to formalise general recursive algorithms in constructive type theory is presented throughout examples. The method separates the computational and logical parts of the definitions. As a consequence, the resulting type-theoretic algorithms are clear, compact and easy to understand. They are as simple as their equivalents in a functional programming language, where there is no restriction on recursive calls. Given a general recursive algorithm, the method consists in defining an inductive special-purpose accessibility predicate that characterises the inputs on which the algorithm terminates. The type-theoretic version of the algorithm can then be defined by structural recursion on the proof that the input values satisfy this predicate. When formalising nested algorithms, the special-purpose accessibility predicate and the type-theoretic version of the algorithm must be defined simultaneously because they depend on each other. Since the method separates the computational part from the logical part of a definition, formalising partial functions becomes also possible.},

year={2003},

keywords={general recursion, partial functions, type theory},

}

** RefWorks **

RT Conference Proceedings

SR Electronic

ID 47405

A1 Bove, Ana

T1 General Recursion in Type Theory

YR 2003

T2 Lecture Notes in Computer Science. International Workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24–28, 2002

SN 978-3-540-14031-3

SP 39

OP 58

AB In this work, a method to formalise general recursive algorithms in constructive type theory is presented throughout examples. The method separates the computational and logical parts of the definitions. As a consequence, the resulting type-theoretic algorithms are clear, compact and easy to understand. They are as simple as their equivalents in a functional programming language, where there is no restriction on recursive calls. Given a general recursive algorithm, the method consists in defining an inductive special-purpose accessibility predicate that characterises the inputs on which the algorithm terminates. The type-theoretic version of the algorithm can then be defined by structural recursion on the proof that the input values satisfy this predicate. When formalising nested algorithms, the special-purpose accessibility predicate and the type-theoretic version of the algorithm must be defined simultaneously because they depend on each other. Since the method separates the computational part from the logical part of a definition, formalising partial functions becomes also possible.

LA eng

DO 10.1007/3-540-39185-1_3

LK http://dx.doi.org/10.1007/3-540-39185-1_3

OL 30