From programming-by-example to proving-by-example

DOI10.1007/3-540-54415-1_56zbMath1493.68167OpenAlexW1515777799MaRDI QIDQ5096230

Masami Hagiya

Publication date: 16 August 2022

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

Full work available at URL: https://doi.org/10.1007/3-540-54415-1_56

Mathematics Subject Classification ID

Computational learning theory (68Q32) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Combinatory logic and lambda calculus (03B40)

Related Items (3)

A typed \(\lambda\)-calculus for proving-by-example and bottom-up generalization procedure ⋮ Towards the animation of proofs -- testing proofs by examples ⋮ The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type

Cites Work

• Synthesis of rewrite programs by higher-order and semantic unification
• Explanation-based generalisation \(=\) partial evaluation
• A unification algorithm for typed \(\overline\lambda\)-calculus
• Proving and applying program transformations expressed with second-order patterns
• Higher-order unification revisited: Complete sets of transformations
• A class of functions synthesized from a finite number of examples and a lisp program scheme
• A Methodology for LISP Program Construction from Examples
• Higher-order unification with dependent function types

This page was built for publication: From programming-by-example to proving-by-example