サクサク読めて、アプリ限定の機能も多数!
トップへ戻る
TGS2024
adam.chlipala.net
This is the web site for the early stages of a book introducing both machine-checked proof with the Coq proof assistant and approaches to formal reasoning about program correctness. Grab a Draft Source on GitHub Quasi-latest PDF draft Quasi-latest source-code tarball Quasi-latest source-code tarball, library only (warning: the author really does not recommend using it in serious projects!) Use in
The logical foundation of Coq is the Calculus of Inductive Constructions, or CIC. In a sense, CIC is built from just two relatively straightforward features: function types and inductive types. From this modest foundation, we can prove essentially all of the theorems of math and carry out effectively all program verifications, with enough effort expended. This chapter introduces induction and recu
Adam Chlipala Arthur J. Conner (1888) Professor of Computer Science Programming Languages & Verification Group (more PL at MIT) Computer Science and Artificial Intelligence Laboratory Department of Electrical Engineering and Computer Science MIT E-mail: adamc@csail.mit.edu Office: 32-G842 Startup update: Nectry is my startup based on Ur/Web and UPO, with a "no-code" product that sets people across
Certified Programming with Dependent Types Introduction Some Quick Examples Introducing Inductive Types Inductive Predicates Infinite Data and Proofs Subset Types and Variations General Recursion More Dependent Types Dependent Data Structures Reasoning About Equality Proofs Generic Programming Universes and Axioms Proof Search by Logic Programming Proof Search in Ltac Proof by Reflection Proving i
In lazy functional programming languages like Haskell, infinite data structures are everywhere. Infinite lists and more exotic datatypes provide convenient abstractions for communication between parts of a program. Achieving similar convenience without infinite lazy structures would, in many cases, require acrobatic inversions of control flow. Laziness is easy to implement in Haskell, where all th
This page compares point-by-point the Objective Caml (OCaml) and Standard ML (SML) programming languages, the two main representatives of the ML programming language family. The comparison includes language design and current tool availability, as well as further social factors. This page isn't meant to be a complete comparison, but rather to highlight differences that might lead to choosing one l
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
3. Arithmetic omega - Presburger arithmetic (propositional formulas, with equalities, inequalities, for nat and Z) auto with arith - ring - associative commutative rewriting field - equalities in commutative fields (like ring, but with division) fourier - linear inequations with propositional structure, on real numbers 4. Induction Introduction (prove inductive facts) apply - treat each constructo
このページを最初にブックマークしてみませんか?
『Adam Chlipala』の新着エントリーを見る
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く