Pnp
Lecture notes for a short course on proving/programming in Coq via SSReflect.
Install / Use
/learn @ilyasergey/PnpREADME
Programs and Proofs
A Short Course on Interactive Proofs in Coq/Ssreflect. This project contains the Coq sources, the lectures and the exercises for the course
"Programs and Proofs: Mechanizing Mathematics with Dependent Types".
The latest draft of the accompanying lecture notes can be downloaded from the official course page:
http://ilyasergey.net/pnp
Initial release: August 2014
Building the Project
Requirements
- Coq (>= "8.10.0" & < "8.12~")
- Mathematical Components
ssreflect(>= "1.10.0" & < "1.12~") - FCSL-PCM (>= "1.0.0" & < "1.3~")
- Hoare Type Theory
Building
We recommend installing the requirements via opam:
opam repo add coq-released https://coq.inria.fr/opam/released
opam pin add coq-htt git+https://github.com/TyGuS/htt\#master --no-action --yes
opam install coq coq-mathcomp-ssreflect coq-fcsl-pcm coq-htt
Then, run make clean; make from the root folder. This will compile
all lecture files, solutions and create the file latex/pnp.pdf with
lecture notes.
Related Skills
YC-Killer
2.7kA library of enterprise-grade AI agents designed to democratize artificial intelligence and provide free, open-source alternatives to overvalued Y Combinator startups. If you are excited about democratizing AI access & AI agents, please star ⭐️ this repository and use the link in the readme to join our open source AI research team.
best-practices-researcher
The most comprehensive Claude Code skills registry | Web Search: https://skills-registry-web.vercel.app
groundhog
398Groundhog's primary purpose is to teach people how Cursor and all these other coding agents work under the hood. If you understand how these coding assistants work from first principles, then you can drive these tools harder (or perhaps make your own!).
isf-agent
a repo for an agent that helps researchers apply for isf funding
