swMATH ID: 19629
Software Authors: Horn, Christian; Smaill, Alan
Description: 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
Homepage: https://pdfs.semanticscholar.org/6cb8/ac778dfdd799dda3e8a0a9169431eef28062.pdf
Keywords: reasoning about specifications; satisfiability; program synthesis; Martin-Löf type theory
Related Software: CLAM; Nuprl; HOL; Isabelle; Coq; Isabelle/HOL; InKa; Lambda-Clam; NQTHM; IsaPlanner; Waldmeister; VAMPIRE; P.rex; OTTER; TRAMP; OMEGA; Flyspeck; Mollusc; fc2tools; Prodigy
Cited in: 34 Publications

Standard Articles

1 Publication describing the Software, including 1 Publication in zbMATH Year
Theorem proving and program synthesis with Oyster. Zbl 0766.68119
Horn, Christian; Smaill, Alan

Citations by Year