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

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

1 2 next

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

1 2 next