Oyster

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 32 articles , 1 standard article )

Showing results 1 to 20 of 32.
Sorted by year (citations)

1 2 next

  1. Johansson, Moa: Lemma discovery for induction. A survey (2019)
  2. Boy de la Tour, Thierry; Peltier, Nicolas: Analogy in automated deduction: a survey (2014)
  3. Wirth, Claus-Peter: Computer-assisted human-oriented inductive theorem proving by \textitdescenteinfinie -- a manifesto (2012)
  4. Monroy, Raúl; Bundy, Alan; Green, Ian: On process equivalence = equation solving in CCS (2009)
  5. Korukhova, Yulia: An approach to automatic deductive synthesis of functional programs (2007)
  6. Ireland, Andrew; Stark, Jamie: Combining proof plans with partial order planning for imperative program synthesis (2006) ioport
  7. Ireland, Andrew; Stark, Jamie: Combining proof plans with partial order planning for imperative program synthesis (2006) ioport
  8. Siekmann, Jörg; Benzmüller, Christoph; Autexier, Serge: Computer supported mathematics with (\Omega)MEGA (2006)
  9. Zinn, Claus: Supporting the formal verification of mathematical texts (2006)
  10. Fiedler, Armin: Natural language proof explanation (2005)
  11. Siekmann, Jörg; Benzmüller, Christoph: (\Omega)MEGA: Computer supported mathematics (2004)
  12. Whittle, Jon; Bundy, Alan; Boulton, Richard: Proofs-as-programs as a framework for the design of an analogy-based ML editor (2002)
  13. Monroy, Raúl: Concept formation via proof planning failure (2001)
  14. Dennis, L. A.; Bundy, A.; Green, I.: Making a productive use of failure to generate witnesses for coinduction from divergent proof attempts (2000)
  15. Monroy, Raúl; Bundy, Alan; Green, Ian: Planning proofs of equations in CCS (2000)
  16. Walther, C.; Kolbe, T.: Proving theorems by reuse (2000)
  17. Dennis, Louise; Bundy, Alan; Green, Ian: Using a generalisation critic to find bisimulations for coinductive proofs (1997)
  18. Basin, David A.; Walsh, Toby: A calculus for and termination of rippling (1996)
  19. Ireland, Andrew; Bundy, Alan: Productive use of failure in inductive proof (1996)
  20. Ireland, Andrew; Bundy, Alan: Extensions to a generalization critic for inductive proof (1996)

1 2 next