Pinned Loading

1. nvim nvim Public

   NeoVim configuration optimized for writing in LaTeX with AI integration for Avante, Lectic, and Claude-Code

   Shell 443 457

2. ModelChecker ModelChecker Public

   A hyperintensional theorem prover for rapidly prototyping modular semantic theories

   Python 13 3

3. .dotfiles .dotfiles Public

   NixOS config

   Nix 3 1

4. BimodalLogic BimodalLogic Public

   Lean 4 formalization of TM, a bimodal logic of tense and modality over task semantics: machine-checked soundness, completeness, compactness, and a tableau decision procedure.

   Lean 7

5. ModalHistory ModalHistory Public

   Graduate seminar on the modern history of modal logic

   TeX 12 2

6. SPSDemo SPSDemo Public

   A Rust crate extracted to Lean 4 by Charon/Aeneas and proved against hand-written specs, behind a reproducible Nix verification gate — the worked demo for the talk "Verified Components from Rust to…

   Lean