Constructive system for automatic program synthesis

DOI10.1016/0304-3975(90)90199-RzbMath0698.68012MaRDI QIDQ912589

Didier Galmiche

Publication date: 1990

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

zbMATH Keywords

program synthesisprogramming proofstyped 6l-calculus

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Combinatory logic and lambda calculus (03B40)

Related Items

On proof normalization in linear logic

Uses Software

• ML
• Automath

Cites Work

• Intuitionism. An introduction
• Theory of symbolic expressions. I
• The system \({\mathcal F}\) of variable types, fifteen years later
• The lambda calculus, its syntax and semantics
• A theory of type polymorphism in programming
• Zur Deutung der intuitionistischen Logik
• Edinburgh LCF. A mechanized logic of computation
• An interpretation of Martin-Löf's type theory in a type-free theory of propositions
• Natural deduction as higher-order resolution
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item