A predicative analysis of structural recursion

DOI10.1017/S0956796801004191MaRDI QIDQ2784165zbMATH OpenFDO

Authors Andreas Abel, Thorsten Altenkirch

Publication date 17 April 2002

Published in Journal of Functional Programming (Search for Journal in Brave)

zbMATH Keywords

lambda calculus

Mathematics Subject Classification ID

Theory of programming languages (68N15) Functional programming and lambda calculus (68N18)

Recommendations

• scientific article; zbMATH DE number 1696606
• CIC $\widehat{~}$ : Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions
• Typed Lambda Calculi and Applications
• Termination checking with types
• Type-based termination of recursive definitions

Cited in

(16)

• scientific article; zbMATH DE number 1696606 (Why is no real title available?)
• Adapting functional programs to higher order logic
• Termination checking with types
• Distributing and parallelizing non-canonical loops
• Proving properties of functional programs by equality saturation
• Inductive prover based on equality saturation for a lazy functional language
• Size-based termination of higher-order rewriting
• Verifying termination and reduction properties about higher-order logic programs
• Compositional coinduction with sized types
• A sound strategy to compile general recursion into finite depth pattern matching
• scientific article; zbMATH DE number 7407785 (Why is no real title available?)
• Well-founded recursion over contextual objects
• Interactive programming in Agda -- objects and graphical user interfaces
• T-rex: termination of recursive functions using lexicographic linear combinations
• Totality for mixed inductive and coinductive types
• scientific article; zbMATH DE number 4085054 (Why is no real title available?)

Describes a project that uses

Uses Software

• Coq

This page was built for publication: A predicative analysis of structural recursion

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