Aaron Stump
Todd Schiller
ABSTRACT
Operational Type Theory (OpTT) is a type theory allowing possibly diverging programs while retaining decidability of type checking and a consistent logic. This is done by distinguishing proofs and (program) terms, as well as formulas and types. The theory features propositional equality on type-free terms, which facilitates reasoning about dependently typed programs. OpTT has been implemented in the Guru verified programming language, which includes a type- and proof-checker, and a compiler to efficient C code. In addition to the core OpTT, Guru implements a number of extensions, including ones for verification of programs using mutable state and input/output. This paper gives an introduction to verified programming in Guru.
- A. Appel. Foundational Proof-Carrying Code. In 16th Annual IEEE Symposium on Logic in Computer Science, 2001. Google Scholar
Digital Library
- E. Barendsen and S. Smetsers. Conventional and Uniqueness Typing in Graph Rewrite Systems. In Proc. 13th Conference on Foundations of Software Technology and Theoretical Computer Science, pages 41--51. Springer-Verlag, 1993. Google ScholarDigital Library
- C. Barrett and C. Tinelli. CVC3. In W. Damm and H. Hermanns, editors, Proceedings of the 19th International Conference on Computer Aided Verification (CAV '07), pages 298--302. Springer-Verlag, 2007. Google ScholarDigital Library
- C. Chen and H. Xi. Combining Programming with Theorem Proving. In Proceedings of the 10th International Conference on Functional Programming (ICFP05), Tallinn, Estonia, September 2005. Google ScholarDigital Library
- R. Harper, F. Honsell, and G. Plotkin. A Framework for Defining Logics. Journal of the Association for Computing Machinery, 40 (1): 143--184, January 1993. Google ScholarDigital Library
- Matthew Hertz and Emery D. Berger. Quantifying the Performance of Garbage Collection vs. Explicit Memory Management. In Proc. 20th Annual ACM SIGPLAN Conference on Object Oriented Programming, Systems, Languages, and Applications, pages 313--326. ACM, 2005. Google ScholarDigital Library
- M. Hofmann and T. Streicher. The groupoid interpretation of type theory. In G. Sambin, editor, Twenty-five years of constructive type theory, pages 83--111. Oxford: Clarendon Press, 1998.Google Scholar
- D. Lee, K. Crary, and R. Harper. Towards a Mechanized Metatheory of Standard ML. In Proc. 34th ACM Symposium on Principles of Programming Languages, pages 173--184. ACM Press, 2007. Google ScholarDigital Library
- D. Licata and R. Harper. A Formulation of Dependent ML with Explicit Equality Proofs. Technical Report CMU-CS-05-178, Carnegie Mellon University School of Computer Science, December 2005.Google Scholar
- C. McBride and J. McKinna. The View from the Left. Journal of Functional Programming, 14 (1), 2004. Google ScholarDigital Library
- M. Moskal. Rocket-Fast Proof Checking for SMT Solvers. In C. Ramakrishnan and J. Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, 2008. Google ScholarDigital Library
- A. Nanevski and G. Morrisett. Dependent Type Theory of Stateful Higher-Order Functions. Technical Report TR-24-05, Harvard University, 2005.Google Scholar
- G. Necula. Proof-Carrying Code. In 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 106--119, January 1997. Google ScholarDigital Library
- U. Norell. Towards a Practical Programming Language Based on Dependent Type Theory. PhD thesis, Chalmers University of Technology, 2007.Google Scholar
- E Pasalic, J. Siek, W. Taha, and S. Fogarty. Concoqtion: Indexed Types Now! In G. Ramalingam and E. Visser, editors, ACM SIGPLAN 2007 Workshop on Partial Evaluation and Program Manipulation, 2007. Google ScholarDigital Library
- A. Petcher. Deciding Joinability Modulo Ground Equations in Operational Type Theory. Master's thesis, Washington University in Saint Louis, May 2008. Available from http://cl.cse.wustl.edu.Google Scholar
- F. Pfenning and C. Schürmann. System Description: Twelf -- A Meta-Logical Framework for Deductive Systems. In 16th International Conference on Automated Deduction, 1999. Google ScholarDigital Library
- Benjamin C. Pierce and David N. Turner. Local type inference. In 25TH ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 252--265, 1998. Google ScholarDigital Library
- T. Sheard. Type-Level Computation Using Narrowing in Ωmega. In Programming Languages meets Program Verification, 2006. Google ScholarDigital Library
- A. Stump. Proof Checking Technology for Satisfiability Modulo Theories. In A. Abel and C. Urban, editors, Logical Frameworks and Meta-Languages: Theory and Practice, 2008.Google Scholar
- A. Stump and D. Oe. Towards an SMT Proof Format. In C. Barrett and L. de Moura, editors, International Workshop on Satisfiability Modulo Theories, 2008. Google ScholarDigital Library
- A. Stump and E. Westbrook. A Core Operational Type Theory. Under review, available from http://www.cs.uiowa.edu/ astump.Google Scholar
- W. Swierstra and T. Altenkirch. Beauty in the Beast. In Haskell Workshop, 2007. Google ScholarDigital Library
- The Coq Development Team. The Coq Proof Assistant Reference Manual, Version V8.0, 2004. http://coq.inria.fr.Google Scholar
- C. Urban, J. Cheney, and S. Berghofer. Mechanising the Metatheory of LF. In Proc. of the 23rd IEEE Symposium on Logic in Computer Science, pages 45--56. IEEE Computer Society, 2008. Google ScholarDigital Library
- K. Watkins, I. Cervesato, F. Pfenning, and D. Walker. A Concurrent Logical Framework I: Judgments and Properties. Technical Report CMU-CS-02-101, Carnegie Mellon University, 2002.Google Scholar
- M. Zeller, A. Stump, and M. Deters. Signature Compilation for the Edinburgh Logical Framework. In C. Schürmann, editor, Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), 2007.Google Scholar
- D. Zhu and H. Xi. Safe Programming with Pointers through Stateful Views. In Proceedings of the 7th International Symposium on Practical Aspects of Declarative Languages, pages 83--97, Long Beach, CA, January 2005. Springer-Verlag LNCS vol. 3350. Google ScholarDigital Library
Index Terms
- Verified programming in Guru
Recommendations
Dependently typed programming with singletons
Haskell '12: Proceedings of the 2012 Haskell SymposiumHaskell programmers have been experimenting with dependent types for at least a decade, using clever encodings that push the limits of the Haskell type system. However, the cleverness of these encodings is also their main drawback. Although the ideas ...
Dependently typed programming with singletons
Haskell '12Haskell programmers have been experimenting with dependent types for at least a decade, using clever encodings that push the limits of the Haskell type system. However, the cleverness of these encodings is also their main drawback. Although the ideas ...
Resource typing in Guru
PLPV '10: Proceedings of the 4th ACM SIGPLAN workshop on Programming languages meets program verificationThis paper presents a resource typing framework for the Guru verified-programming language, in which abstractions for various kinds of program resources can be defined. Implemented examples include reference-counted data, mutable arrays, and heap-...
Comments