This interactive tutorial will teach you how to use the sequent calculus, a simple set of rules with which you can use to show the truth of statements in first order logic. It is geared towards anyone with some background in writing software for computers, with knowledge of basic boolean logic.
Adam Chlipala This is the web site for an in-progress textbook about practical engineering with the Coq proof assistant. The focus is on building programs with proofs of correctness, using dependent types and scripted proof automation. This is the text for a Fall 2008 class at Harvard.
The goal of the Ynot project is to make programming with dependent types practical for a modern programming language. In particular, we are extending the Coq proof assistant to make it possible to write higher-order, imperative and concurrent programs (in the style of Haskell) through a shallow embedding of Hoare Type Theory (HTT). HTT provides a clean separation between pure and effectful computations, makes it possible to formally specify and reason about effects, and is fully compositional. This seems like it's related to Adam Chlipala's A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language. See, in particular, slides 23-24 of this presentation (PDF). More generally, computation and reflection seem to be gaining recognition as important features for the practical use of Coq Again, the point is to simplify programming with dependent types in Coq
Research Interests Programming Languages, Logic and Type Theory, Logical Frameworks, Automated Deduction, Trustworthy Computing (see also Publications, Students & Co-authors) Projects Logosphere A Formal Digital Library Triple Type Refinement in Programming Languages ConCert Language Technology for Trustless Software Dissemination Twelf Logical and Meta-Logical Frameworks SeLF Distributed System Security via Logical Frameworks Manifest Security Logics and Languages for Manifestly Secure Systems Prospero Integrating Types and Specifications
Coq'Art is the familiar name for the first book on the Coq proof assistant and its underlying theory the Calculus of Inductive Constructions , written by Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development Coq'Art: The Calculus of Inductive Constructions Series: Texts in Theoretical Computer Science. An EATCS Series Bertot, Yves, Castéran, Pierre 2004, XXV, 469 p., Hardcover ISBN: 3-540-20854-2 This site has been updated for Coq8.2. Warning! Some solutions we propose don't work on versions prior to V8.2gamma. Please find here a tar file fully compatible with coq8.1pl3 and the printed edition of the book. These exercises were written after the release of the book (May 2004). The solution of some of them (e.g. mergesort ) illustrates new features of Coq. For instance, command Function and tactic functional induction.
Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. Isabelle is developed at University of Cambridge (Larry Paulson) and Technische Universität München (Tobias Nipkow). See the Isabelle overview for a brief introduction. Now available: Isabelle2008 Some notable improvements: * HOL: significant speedup of Metis prover; proper support for multithreading. * HOL: new version of primrec command supporting type-inference and local theory targets. * HOL: improved support for termination proofs of recursive function definitions. * New local theory targets for class instantiation and overloading. * Support for named dynamic lists of theorems.
Supported and ongoing software projects: * IsaPlanner - a proof planner for Isabelle * HiGraph - a system for presenting and manipulating hierarchical proofs/graphs generated by proof planning in IsaPlanner. Currently just an editor/drawing tool for the graphs. * Quantomatic - a tool for graphically reasoning about quantum computation using models based on compact closed categories. Older software projects (no longer being developed): * Lambda Clam - a proof planner written in lambda prolog. * HR - an automated theory formation system * Clam proof planner with oyster - a proof planner written in prolog * Clam version 3.2 * HOL-Clam - a link up between the HOL proof assistant and the Clam proof planner. * Anastasia - a structural program editor * Press - a prolog based system for solving symbolic, transcendental, non-differential equations
IsaPlanner is a generic framework for proof planning in the interactive theorem prover Isabelle. It facilitates the encoding of reasoning techniques, which can be used to conjecture and prove theorems automatically. The system provides an interactive tracing tool that allows you to interact the proof planning attempt. (see the screenshot of IsaPlanner being used with Isabelle and Proof General) It is based on the Isabelle theorem prover and the Isar language. The main proof technique written in IsaPlanner is an inductive theorem prover based on Rippling. This is applicable within Isabelle's Higher Order Logic, and can easily be adapted to Isabelle's other logics. The system now the main platform for proof planning research in the Edinburgh mathematical reasoning group
This site is an experimental HTML rendering of fragments of the IsarMathLib project. IsarMathLib is a library of mathematical proofs formally verified by the Isabelle theorem proving environment. The formalization is based on the Zermelo-Fraenkel set theory. The Introduction provides more information about IsarMathLib. The software for exporting Isabelle's Isar language to HTML markup is at an early beta stage, so some proofs may be rendered incorrectly. In case of doubts, compare with the Isabelle generated IsarMathLib proof document.
In the fully expansive (or LCF-style) approach to theorem proving, theorems are represented by an abstract type whose primitive operations are the axioms and inference rules of a logic. Theorem proving tools are implemented by composing together the inference rules using ML programs. This idea can be generalised to computing valid judgements that represent other kinds of information. In particular, consider judgements (a,r,t,b), where a is a set of boolean terms (assumptions) that are assumed true, r represents a variable order, t is a boolean term all of whose free variables are boolean and b is a BDD. Such a judgement is valid if under the assumptions a, the BDD representing t with respect to r is b, and we will write a r t --> b when this is the case. The derivation of "theorems" like a r t --> b can be viewed as "proof" in the style of LCF by defining an abstract type term_bdd that models judgements a r t --> b analogously to the way the type thm models theorems |- t.
T. Mossakowski, und A. Tarlecki. 17th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), Volume 8412 von Lecture Notes in Computer Science, Seite 441-456. Springer-Verlag Berlin Heidelberg, (2014)
T. Mossakowski, A. Haxthausen, D. Sannella, und A. Tarlecki. Logics of formal specification languages, Volume 22 von Monographs in Theoretical Computer Science, Kapitel 3, Springer-Verlag Heidelberg, (2008)
T. Mossakowski, P. Hoffman, S. Autexier, und D. Hutter. CASL Reference Manual, Volume 2960 von Lecture Notes in Computer Science, Kapitel ÏV, Springer Verlag, London, Ëdited by T. Mossakowski.(2004)
T. Mossakowski, C. Maeder, und K. Lüttich. TACAS 2007, Volume 4424 von Lecture Notes in Computer Science, Seite 519-522. Springer-Verlag Heidelberg, (2007)
M. Codescu, und T. Mossakowski. Algebra and Coalgebra in Computer Science, CALCO'11, Volume 6859 von Lecture Notes in Computer Science, Seite 145-160. Springer, (2011)