Terminating general recursion

DOI10.1007/BF01941137zbMath0659.68020MaRDI QIDQ1112584

Bengt Nordström

Publication date: 1988

Published in: BIT (Search for Journal in Brave)

zbMATH Keywords

fixed pointfunctional programmingMartin-Löf's type theorytermination proofprogramming logicproof rulegeneral recursion operatorwell-founded induction

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) General topics in the theory of software (68N01)

Related Items (13)

Inductive families ⋮ Formal derivation of greedy algorithms from relational specifications: a tutorial ⋮ Set theory for verification. II: Induction and recursion ⋮ Do-it-yourself type theory ⋮ Certified CYK parsing of context-free languages ⋮ Program development in constructive type theory ⋮ Partiality and recursion in interactive theorem provers – an overview ⋮ Using Structural Recursion for Corecursion ⋮ Algebra of programming in Agda: Dependent types for relational program derivation ⋮ A Decision Procedure for Regular Expression Equivalence in Type Theory ⋮ Normalising the associative law: An experiment with Martin-Löf's type theory ⋮ Inductive and Coinductive Components of Corecursive Functions in Coq ⋮ Synthesis of ML programs in the system Coq

Uses Software

• Nuprl

Cites Work

• Unnamed Item
• Unnamed Item
• Propositions and specifications of programs in Martin-Löf's type theory
• Constructing recursion operators in intuitionistic type theory
• Lessons learned from LCF: A Survey of Natural Deduction Proofs

This page was built for publication: Terminating general recursion