Extraction of redundancy-free programs from constructive natural deduction proofs

DOI10.1016/S0747-7171(08)80139-3zbMath0731.68079MaRDI QIDQ808284

Yukihide Takayama

Publication date: 1991

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

zbMATH Keywords

constructive logicprogram verificationautomated programmingproof treesrealizability interpretationredundancy-free codes

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

First order marked types ⋮ Defining concurrent processes constructively ⋮ \(QPC_ 2\): A constructive calculus with parameterized specifications

Uses Software

• Nuprl

Cites Work

• The calculus of constructions
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item