sftypes / Software Foundations
Coq proofs of exercises in Pierce's book
Labels
Projects that are alternatives of or similar to Software Foundations
topology
General topology in Coq [maintainers=@amiloradovsky,@Columbus240,@stop-cran]
Stars: ✭ 36 (+620%)
Mutual labels: coq
Practical Fm
A gently curated list of companies using verification formal methods in industry
Stars: ✭ 272 (+5340%)
Mutual labels: coq
Set-Theory
Coq encoding of ZFC and formalization of the textbook Elements of Set Theory
Stars: ✭ 55 (+1000%)
Mutual labels: coq
Unimath
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
Stars: ✭ 680 (+13500%)
Mutual labels: coq
Coq
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
Stars: ✭ 3,566 (+71220%)
Mutual labels: coq
Verdi
A framework for formally verifying distributed systems implementations in Coq
Stars: ✭ 496 (+9820%)
Mutual labels: coq
Company Coq
A Coq IDE build on top of Proof General's Coq mode
Stars: ✭ 297 (+5840%)
Mutual labels: coq
Category Theory
An axiom-free formalization of category theory in Coq for personal study and practical work
Stars: ✭ 562 (+11140%)
Mutual labels: coq
Software Foundations
Our answers to exercises in http://www.cis.upenn.edu/~bcpierce/sf
Setting up your machine to do the exercises
-
Install Coq: http://coq.inria.fr/download
-
Configure vim for interactive proof
" using Vundle for modules Bundle 'def-lkb/vimbufsync' Bundle 'the-lambda-church/coquille' " configure key bindings and colors augroup coqColors autocmd! autocmd BufReadPost *.v hi CheckedByCoq ctermbg=17 guibg=#111133 autocmd BufReadPost *.v hi SentToCoq ctermbg=60 guibg=#222244 augroup END map <silent> <leader>cs :CoqLaunch<cr> map <silent> <leader>cg :CoqToCursor<cr> map <silent> <leader>cn :CoqNext<cr> map <silent> <leader>cu :CoqUndo<cr> map <silent> <leader>cq :CoqKill<cr> map <silent> <leader>cx <C-w>l<C-w>L<C-w>t<C-w>K map <silent> <leader>cp :execute "Coq Print " . expand("<cword>") . "."<cr>
-
Download a copy of the book http://www.cis.upenn.edu/~bcpierce/sf/sf.tar.gz
Edit and submit exercises.
- Start with
Basics.v, fill in the blanks, and ensure it passes the proof assistant:coqc Basics.v - Rename it to
[your_github_name]_Basics.vand submit it as a pull request to this repo.
Note that the project description data, including the texts, logos, images, and/or trademarks,
for each open source project belongs to its rightful owner.
If you wish to add or remove any projects, please contact us at [email protected].