Oyster 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.68119Horn, Christian; Smaill, Alan 1992 all top 5 Cited by 43 Authors 12 Bundy, Alan 7 Smaill, Alan 4 Green, Ian 4 van Harmelen, Frank 3 Basin, David A. 3 Horn, Christian 3 Ireland, Andrew 3 Monroy, Raúl 2 Benzmüller, Christoph Ewald 2 Dennis, Louise Abigail 2 Hesketh, Jane 2 Kraan, Ina 2 Siekmann, Jörg H. 2 Stevens, Andrew 2 Walsh, Toby 1 Arts, Thomas 1 Autexier, Serge 1 Boulton, Richard J. 1 Boy de la Tour, Thierry 1 Busch, Holger 1 Fiedler, Armin 1 Gauthier, Thibault 1 Giesl, Jürgen 1 Hamami, Yacin 1 Johansson, Moa 1 Kaliszyk, Cezary 1 Kerber, Manfred 1 Kolbe, Thomas H. 1 Korukhova, Yulia 1 Kumar, Ramana 1 Morris, Rebecca Lea 1 Norrish, Michael 1 Peltier, Nicolas 1 Präcklein, Axel 1 Richards, Bradley L. 1 Sengler, Claus 1 Subramanian, Sakthi 1 Urban, Josef 1 Walther, Christoph 1 Whittle, Jon 1 Wiggins, Geraint A. 1 Wirth, Claus-Peter 1 Zinn, Claus all top 5 Cited in 9 Serials 7 Journal of Automated Reasoning 3 Annals of Mathematics and Artificial Intelligence 2 Artificial Intelligence 2 Journal of Applied Logic 1 Formal Aspects of Computing 1 Formal Methods in System Design 1 1 Logic Journal of the IGPL 1 The Review of Symbolic Logic Cited in 4 Fields 34 Computer science (68-XX) 9 Mathematical logic and foundations (03-XX) 1 General and overarching topics; collections (00-XX) 1 History and biography (01-XX) Citations by Year