Jonathan Aldrich
Robert J. Simmons
Key Shin
ABSTRACT
Teaching and learning formal programming language theory is hard, in part because it's easy to make mistakes and hard to find them. Proof assistants can help check proofs, but their learning curve is too steep to use in most classes, and is a barrier to researchers too.
In this paper we present SASyLF, an LF-based proof assistant specialized to checking theorems about programming languages and logics. SASyLF has a simple design philosophy: language and logic syntax, semantics, and meta-theory should be written as closely as possible to the way it is done on paper. We describe how we designed the SASyLF syntax to be accessible to students learning type theory, and how students can understand its semantics directly in terms of the theory they are taught in class. SASyLF can express proofs typical of an introductory graduate type theory course. SASyLF proofs are generally very explicit, but its built-in support for variable binding provides substitution properties for free and avoids awkward variable encodings. We describe preliminary experience teaching with SASyLF.
- Andreas Abel, Bor-Yuh Evan Chang, and Frank Pfenning. Human-Readable, Machine-Verifiable Proofs for Teaching Constructive Logic. In Workshop on Proof Transformations, Proof Presentations and Complexity of Proofs (PTP'01), June 2001.Google Scholar
- Brian Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack, and Stephanie Weirich. Engineering Formal Metatheory. In Symposium on Principles of Programming Languages, 2008. Google ScholarDigital Library
- Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve Zdancewic. Mechanized Metatheory for the Masses: The PoplMark Challenge. In Theorem Proving in Higher Order Logics, pages 50--65, 2005. Google ScholarDigital Library
- Ian Barland, Matthias Felleisen, Kathi Fisler, Phokion Kolaitis, and Moshe Y. Vardi. Integrating Logic into the Computer Science Curriculum. http://www.cs.utexas.edu/\verb1 1csed/FM/docs/iticse--fislervardi.pdf, 2000.Google Scholar
- Jon Barwise and John Etchemendy. Computers, Visualization, and the Nature of Reasoning. In The Digital Phoenix: How Computers are Changing Philosophy, pages 93--116. Blackwell, 1998.Google Scholar
- Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development. Springer-Verlag, 2004. Google ScholarDigital Library
- Carl Eastlund, Dale Vaillancourt, and Matthias Felleisen. ACL2 for Freshmen: First Experiences. In ACL2 Workshop, 2007.Google Scholar
- Andrew Gacek. The Abella Interactive Theorem Prover (system description). In IJCAR, 2008. Google ScholarDigital Library
- D. Goldson and S. Reeves. Using Programs to Teach Logic to Computer Scientists. Notices of the American Mathematical Society, 40: 143--148, 1993.Google Scholar
- Robert Harper. Practical Foundations for Programming Languages. Available at http://www.cs.cmu.edu/~rwh/plbook/book.pdf, 2008. Google ScholarDigital Library
- Robert Harper, Furio Honsell, and Gordon D. Plotkin. A Framework for Defining Logics. phJ. ACM, 40 (1): 143--184, 1993. Google ScholarDigital Library
- Jacob Matthews, Robert Bruce Findler, Matthew Flatt, and Matthias Felleisen. A Visual Environment for Developing Context-Sensitive Term Rewriting Systems. In International Conference on Rewriting Techniques and Applications. Springer Verlag LNCS 3091, 2004.Google Scholar
- Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL: A Proof Assistant For Higher-Order Logic. Lecture Notes in Computer Science, 2283, 2002. Google ScholarDigital Library
- Mikael Pettersson. Compiling Natural Semantics. PhD thesis, Linkoping University, 1995. Google ScholarDigital Library
- Frank Pfenning. Logical Frameworks. In Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, chapter 17, pages 1063--1147. Elsevier Science and MIT Press, 2001. Google ScholarDigital Library
- Frank Pfenning. Computation and Deduction. Cambridge University Press. In preparation. Draft from April 1997 available electronically at http://www.cs.cmu.edu/~twelf/notes/cd.ps.Google Scholar
- Frank Pfenning and Carsten Schürmann. System Description: Twelf - A Meta-Logical Framework for Deductive Systems. In International Conference on Automated Deduction, pages 202--206, July 1999. Google ScholarDigital Library
- Richard Scheines and Wilfried Sieg. Computer Environments for Proof Construction. Interactive Learning Environments, 4: 159--169, 1994.Google ScholarCross Ref
- Carsten Schürmann. Automating the Meta-Theory of Deductive Systems. PhD thesis, Carnegie Mellon University, 2000.Google Scholar
- Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Tom Ridge, Susmit Sarkar, and Rok Strnisa. Ott: Effective Tool Support for the Working Semanticist. In International Conference on Functional Programming, pages 1--12, 2007. Google ScholarDigital Library
- Richard Sommer and Gregory Nuckols. A Proof Environment for Teaching Mathematics. J. Autom. Reason., 32 (3): 227--258, 2004. Google ScholarDigital Library
- S. Tobias. Revitalizing Undergraduate Science: Why some things work and most don't. Research Corporation, 1992.Google Scholar
- Masaru Tomita. An Efficient Augmented-Context-Free Parsing Algorithm. phComputational Linguistics, 13 (1-2): 31--46, 1987. Google ScholarDigital Library
- Mark van den Brand, Jan Heering, Paul Klint, and Pieter Olivier. Compiling Rewrite Systems: The ASF+SDF Compiler. Transactions on Software Engineering and Methodology, 24: 334--368, 2002. Google ScholarDigital Library
Index Terms
- SASyLF: an educational proof assistant for language theory
Recommendations
The Reflective Milawa Theorem Prover is Sound (Down to the Machine Code that Runs it)
This paper presents, we believe, the most comprehensive evidence of a theorem prover's soundness to date. Our subject is the Milawa theorem prover. We present evidence of its soundness down to the machine code. Milawa is a theorem prover styled after ...
A Framework for Defining Logical Frameworks
In this paper, we introduce a General Logical Framework, called GLF, for defining Logical Frameworks, based on dependent types, in the style of the well known Edinburgh Logical Framework LF. The framework GLF features a generalized form of lambda ...
A List-machine Benchmark for Mechanized Metatheory
We propose a benchmark to compare theorem-proving systems on their ability to express proofs of compiler correctness. In contrast to the first POPLmark, we emphasize the connection of proofs to compiler implementations, and we point out that much can be ...
Comments