Specification and verification of a formal system for structurally recursive functions

DOI10.1007/3-540-44557-9_1MaRDI QIDQ2766795zbMATH OpenFDO

Authors Andreas Abel

Publication date 22 July 2002

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-44557-9_1

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• A predicative analysis of structural recursion
• Type-based termination of recursive definitions
• Inductively defined functions in functional programming languages
• Termination checking with types
• Simple general recursion in type theory

Cited in

(8)

• Inductively defined functions in functional programming languages
• A predicative analysis of structural recursion
• A Structure-directed Total Correctness Proof Rule for Recursive Procedure Calls
• Termination checking with types
• Well-founded recursion over contextual objects
• Compositional coinduction with sized types
• A sound strategy to compile general recursion into finite depth pattern matching
• Verifying termination and reduction properties about higher-order logic programs

This page was built for publication: Specification and verification of a formal system for structurally recursive functions

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