Programming by example and proving by example using higher-order unification

DOI10.1007/3-540-52885-7_116MaRDI QIDQ6488562zbMATH OpenFDO

Authors Masami Hagiya

Publication date 28 April 2023

Full work available at URL https://doi.org/10.1007/3-540-52885-7_116

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• From programming-by-example to proving-by-example
• Synthesis of rewrite programs by higher-order and semantic unification
• Example-directed synthesis: a type-theoretic interpretation
• A knowledge-based approach to program synthesis from examples
• A typed -calculus for proving-by-example and bottom-up generalization procedure

Cites work

• A class of functions synthesized from a finite number of examples and a lisp program scheme
• A Methodology for LISP Program Construction from Examples
• A unification algorithm for typed \(\bar\lambda\)-calculus
• Edinburgh LCF. A mechanized logic of computation
• Generalization from partial parametrization in higher-order type theory
• Higher-order unification revisited: Complete sets of transformations
• Higher-order unification with dependent function types
• scientific article; zbMATH DE number 4180832 (Why is no real title available?)
• scientific article; zbMATH DE number 3859117 (Why is no real title available?)
• scientific article; zbMATH DE number 4051039 (Why is no real title available?)
• scientific article; zbMATH DE number 3688776 (Why is no real title available?)
• scientific article; zbMATH DE number 3735770 (Why is no real title available?)
• Natural deduction as higher-order resolution
• Proving and applying program transformations expressed with second-order patterns
• The calculus of constructions
• The Inference of Regular LISP Programs from Examples

Cited in

(6)

• Generalization from partial parametrization in higher-order type theory
• Example-directed synthesis: a type-theoretic interpretation
• Editing by example
• From programming-by-example to proving-by-example
• A typed -calculus for proving-by-example and bottom-up generalization procedure
• Synthesis of rewrite programs by higher-order and semantic unification

This page was built for publication: Programming by example and proving by example using higher-order unification

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