oysteikt/tapl-proofs
0
0
Fork 0
Code Issues Pull Requests Activity
14 Commits 1 Branch 0 Tags
bbc0046d5d0534d0750abf34bc52554d2874a74c
T
Clone
Open with VS Code Open with VSCodium Open with Intellij IDEA
Download ZIP Download TAR.GZ Download BUNDLE
oysteikt bbc0046d5d chap11: progress
2026-07-01 02:35:58 +09:00
src
chap11: progress
2026-07-01 02:35:58 +09:00
.envrc
Initial commit
2026-06-24 21:36:42 +09:00
.gitignore
.gitignore: ignore nix results and rocq caches
2026-07-01 02:35:41 +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%