Modelling general recursion in type theory

DOI10.1017/S0960129505004822MaRDI QIDQ5697711zbMATH OpenFDO

Authors Ana Bove, Venanzio Capretta

Publication date 18 October 2005

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

Full work available at URL https://doi.org/10.1017/S0960129505004822

zbMATH Keywords

constructive type theorygeneral recursive algorithmstype-theoretic algorithms

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 2003149
• scientific article; zbMATH DE number 883893
• Simple general recursion in type theory
• Another look at function domains
• scientific article; zbMATH DE number 1863381

Cited in

(22)

• Terminating general recursion
• Typing total recursive functions in Coq
• Recursive coalgebras from comonads
• Simple general recursion in type theory
• Another look at function domains
• Inductive and coinductive components of corecursive functions in Coq
• scientific article; zbMATH DE number 5142784 (Why is no real title available?)
• A Type of Partial Recursive Functions
• Algebra of programming in Agda: Dependent types for relational program derivation
• scientific article; zbMATH DE number 4126684 (Why is no real title available?)
• scientific article; zbMATH DE number 2003149 (Why is no real title available?)
• scientific article; zbMATH DE number 1863381 (Why is no real title available?)
• scientific article; zbMATH DE number 827981 (Why is no real title available?)
• A Generalized Modality for Recursion
• Dependent Types at Work
• General Recursion via Coinductive Types
• Automating Side Conditions in Formalized Partial Functions
• Partiality and recursion in interactive theorem provers -- an overview
• Coalgebras in functional programming and type theory
• Primitive recursive dependent type theory
• High-level modelling for typed functional programming
• Partial and nested recursive function definitions in higher-order logic

Describes a project that uses

Uses Software

• Automath

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5697711)