Theorem proving and program synthesis with Oyster. Martin-Löf type theory provides a formal framework for the construction of verified programs, both specified and written in the type theory. We describe an implementation of the type theory that aims to provide an environment for software engineering using this approach. We illustrate this by describing the synthesis of a simple evaluator of arithmetic expressions in the system

References in zbMATH (referenced in 34 articles , 1 standard article )

Showing results 21 to 34 of 34.
Sorted by year (citations)
  1. Ireland, Andrew; Bundy, Alan: Extensions to a generalization critic for inductive proof (1996)
  2. Ireland, Andrew; Bundy, Alan: Productive use of failure in inductive proof (1996)
  3. Kerber, Manfred; Präcklein, Axel: Using tactics to reformulate formulae for resolution theorem proving (1996)
  4. Kraan, Ina; Basin, David; Bundy, Alan: Middle-out reasoning for synthesis and induction (1996)
  5. Sengler, Claus: Termination of algorithms over non-freely generated data types (1996)
  6. Subramanian, Sakthi: Mechanical verification on strategies (1995)
  7. Basin, David A.; Walsh, Toby: Termination orderings for rippling (1994)
  8. Busch, Holger: Rule-based induction (1994)
  9. Horn, Christian; Smaill, Alan: From meta-level tactics to object-level programs (1994)
  10. Richards, Bradley L.; Kraan, Ina; Smaill, Alan; Wiggins, Geraint A.: \textitMollusc: a general proof-development shell for sequent-based logics (1994)
  11. Bundy, Alan; Stevens, Andrew; van Harmelen, Frank; Ireland, Andrew; Smaill, Alan: Rippling: A heuristic for guiding inductive proofs (1993)
  12. Horn, Christian; Smaill, Alan: Theorem proving and program synthesis with Oyster (1992)
  13. Bundy, Alan; van Harmelen, Frank; Hesketh, Jane; Smaill, Alan: Experiments with proof plans for induction (1991)
  14. Bundy, Alan; van Harmelen, Frank; Hesketh, Jane; Smaill, Alan; Stevens, Andrew: A rational reconstruction and extension of recursion analysis (1989)