On automating the extraction of programs from proofs using product types

DOI10.1016/S1571-0661(04)80551-6zbMath1261.68045OpenAlexW2092505298WikidataQ58001562 ScholiaQ58001562MaRDI QIDQ4916212

Fairouz Kamareddine, Mauricio Ayala-Rincón, François Monin

Publication date: 19 April 2013

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

Full work available at URL: https://doi.org/10.1016/s1571-0661(04)80551-6

zbMATH Keywords

program extractionproduct typesautomated termination

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Combinatory logic and lambda calculus (03B40)

Cites Work

• Recursive programming with proofs
• Automatizing termination proofs of recursively defined functions
• Termination of nested and mutually recursive algorithms
• Typing and computational properties of lambda expressions
• An ordinal measure based procedure for termination of functions
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: On automating the extraction of programs from proofs using product types