oysteikt/tapl-proofs
0
0
Fork 0
Code Issues Pull Requests Activity
8 Commits 1 Branch 0 Tags
55b973fd5fbc2738b96fb2d2c96a280d803c7c44
T
Clone
Open with VS Code Open with VSCodium Open with Intellij IDEA
Download ZIP Download TAR.GZ Download BUNDLE
oysteikt 55b973fd5f chap4: init
2026-06-26 18:21:52 +09:00
src
chap4: init
2026-06-26 18:21:52 +09:00
.envrc
Initial commit
2026-06-24 21:36:42 +09:00
flake.lock
Initial commit
2026-06-24 21:36:42 +09:00
flake.nix
flake.nix: add ocaml tooling
2026-06-26 18:21:42 +09:00
README.md
Initial commit
2026-06-24 21:36:42 +09:00

README.md

TaPL proofs

This repository contains various exercises from the book "Types and Programming Languages", solved in Rocq.

I'm pretty new to the entire Rocq ordeal while solving this, so I would not encourage using this as a reference solution.

Reference in New Issue View Git Blame Copy Permalink
S
Description
Exercises from "Types and Programming Languages"
Readme 107 KiB
Languages
Rocq Prover 90.8%
OCaml 8.5%
Nix 0.7%