A user's friendly syntax to define recursive functions as typed λ-terms

DOI10.1007/3-540-60579-7_5zbMath1530.68062MaRDI QIDQ6061875

Pascal Manoury

Publication date: 8 December 2023

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

zbMATH Keywords

recursive functiondata typeintroduction ruleinduction hypothesisinductive variable

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Combinatory logic and lambda calculus (03B40) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• Unnamed Item
• Unnamed Item
• The lambda calculus, its syntax and semantics
• Recursive programming with proofs
• Automatizing termination proofs of recursively defined functions
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES

This page was built for publication: A user's friendly syntax to define recursive functions as typed λ-terms