Machine Logic
At the junction of computation, logic and mathematics
Tag: Coq
Porting libraries of mathematics between proof assistants
(14 Sep 2022)
Axiomatic type classes: some history, some examples
(02 Mar 2022)
ALEXANDRIA: Large-Scale Formal Proof for the Working Mathematician
(08 Dec 2021)