Certified Programming with Dependent Types
This is the web site for a 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. I'm following an unusual philosophy in this book, so it may be of interest even to long-time Coq users. At the same time, I hope that it provides an easier introduction for newcomers, since s
Index of /pub/Presen
Name Last modified Size Description Parent Directory 13-Nov-2007 07:33 - ACM-ICPC-Algorithm.ppt 18-Dec-2007 10:44 166k ATTAPL-20060621.ppt 18-Dec-2007 10:44 169k ATTAPL9-3.ppt 18-Dec-2007 10:44 116k CIAA2008.ppt 24-Jul-2008 16:10 219k D-5W1H.ppt 10-Jan-2008 15:37 609k PLANX2007.ppt 10-Jan-2008 15:38 298k PLANX2008.ppt 10-Jan-2008 15:38 169k POPL-20060531.ppt 18-Dec-2007 10:46 104k POPL200
The CompCert verified compiler
The CompCert verified compiler Commented Coq development Version 3.13, 2023-07-04 Introduction CompCert is a compiler that generates ARM, PowerPC, RISC-V and x86 assembly code from CompCert C, a large subset of the C programming language. The particularity of this compiler is that it is written mostly within the specification language of the Coq proof assistant, and its correctness --- the fact th
Coqで依存型 - にわとり小屋でのプログラミング
最近Agdaがはやっているみたいなので、Coqでも依存型（dependent type）を使ってみた。 実装したのは長さ n のベクトル型だ。このベクトル型を使うと、空でないとか、長さが等しいとかを型の段階で保証できるので、より安全なプログラムを書くことができるのだ。 Variable A:Set. Inductive Vec : nat -> Set := | VNil : Vec O | VCons : forall n, A -> Vec n -> Vec (S n). このベクトル型を使えば、コンパイル時に長さの整合性もチェックしてくれて、間違いがある場所を教えてくれる。コンパイルさえ通れば、OutOfBoundsExceptionのような実行時エラーは起こりえないことが保証される。 例えば、一般的にリストのhead関数は、引数が1以上の長さのときのみ定義でき、空リストの場合には値
Lambda Tamer
The Lambda Tamer project tackles the issues surrounding computer formalization of programming languages and their tools, based around the Coq proof assistant. The Lambda Tamer methodology centers on higher-order and dependently-typed abstract syntax and aggressive automation. The main project output is a library of Coq definitions, theorems, and tactics in support of building certified compilers f
Tutorial Materials for Programming Language Research
Getting started: You will need the following software. Coq: Version 8.1 or a later release. Binary and source packages are available from the Coq homepage. Either CoqIDE (comes with Coq) or Proof General. Both provide interactive environments for developing proofs and are easier to work with than Coq's toploop. coq-tutorial.zip, which contains all the Coq files and documentation for this tutorial.
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
Ynot
Matthieu Sozeau :: Russell
http://pages.cs.wisc.edu/~mulhern/coqtalks/index.html
Coq - Correctness of an Expression Compiler : programming
Interactive Computer Theorem Proving
http://www.cs.virginia.edu/~wh5a/coq/SimpTypLCalc/STLC.v
Proving with Computer Assistance