Modelling general recursion in type theory

DOI10.1017/S0960129505004822zbMath1084.03026MaRDI QIDQ5697711

Ana Bove, Venanzio Capretta

Publication date: 18 October 2005

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

zbMATH Keywords

constructive type theorygeneral recursive algorithmstype-theoretic algorithms

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Second- and higher-order arithmetic and fragments (03F35)

Related Items (11)

Typing total recursive functions in Coq ⋮ Coalgebras in functional programming and type theory ⋮ A Type of Partial Recursive Functions ⋮ Partiality and recursion in interactive theorem provers – an overview ⋮ Partial and nested recursive function definitions in higher-order logic ⋮ Recursive coalgebras from comonads ⋮ Dependent Types at Work ⋮ Another Look at Function Domains ⋮ Algebra of programming in Agda: Dependent types for relational program derivation ⋮ Automating Side Conditions in Formalized Partial Functions ⋮ Inductive and Coinductive Components of Corecursive Functions in Coq

Uses Software

• Automath

This page was built for publication: Modelling general recursion in type theory