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. more...
A Tutorial Implementation of a Dependently Typed Lambda Calculus Andres Löh, Conor McBride and Wouter Swierstra We present the type rules for a dependently-typed core calculus together with a straightforward implementation in Haskell. We explicitly highlight the changes necessary to shift from a simply-typed lambda calculus to the dependently-typed lambda calculus. We also describe how to extend our core language with data types and write several small example programs. The paper is accompanied by an executable interpreter and example code that allows immediate experimentation with the system we describe. Download Draft Paper (submitted to FI) Haskell source code (executable Haskell file containing all the code from the paper plus the interpreter; automatically generated from the paper sources) prelude.lp (prelude for the LambdaPi interpreter, containing several example programs) Instructions (how to get started with the LambdaPi interpreter)
The Haskell project was begun in order to unify "more than a dozen non-strict, purely functional programming languages". (mirror) We are rapidly approaching that many viable choices for programming with dependent types. 1. Epigram 2. ATS (successor to Dependent ML) 3. Agda (successor to Cayenne) 4. Ωmega 5. NuPrl 6. Twelf 7. Isabelle 8. Coq etc caveats * Some of the items on this list are theorem provers first and dependently-typed programming languages second. Adam Chlipala argues that this is not such a problem for Coq. * Some of these choices may not be real options for programing with dependent types. Twelf is designed for programming about programming languages, and, if I remember correctly, doesn't have parametric polymorphism because of something having to do with higher-order abstract syntax. Is it time yet to do anything about the cornucopia of options? see comments
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
Small TYPES workshop Curry-Howard Implementation Techniques/Connecting Humans and Type-checkers 2006 The CHIT Workshop discuss implementation issues.Keywords: * Terms and binders * Type inference, type constraints and unification * Reduction, evaluation and compilation * Proof refinement/Proof engine * State handling, library, modules, saving format * Coercions * Termination checking The CHAT workshop will focus on interaction between users and proof environments, graphical interfaces, and on network-based interaction. Keywords: * Declarative versus procedural proof styles (structured proofs, XML) * Web based interfaces (including cooperative environments) * Libraries and information retrieval (including search engines) * Proof documentation (literate proving) * Protocols for UI-interaction
Russell is a language for programming with dependent types in Coq. It uses an adaptation of the predicate subtyping feature of PVS to allow users to write only algorithmic code while using strong specifications. Proof obligations are generated automatically, and, once proved, permit to build a complete, valid Coq term. As an example of using Russell to develop programs with dependent types, I implemented the Finger Tree data structure [3] in Coq. It gives quite a few insights about the power of dependent types for specification and their practical use [4]. Here's the relevant page. You can have a look at the example on celebrities in a party inspired by Richard Bird's article. Yet a lighter example: quicksort. I developed a complete formalization [5] of simply-typed lambda calculus with constants in the dependently-typed style with the help of Program. It includes a tait-style proof of weak normalization.
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.