Code
Software verification
- Refinement logic for fine-grained concurrency
- Calculating weakest precondition for relative completeness of Hoare logic
(
darcs get http://cs.ru.nl/~dfrumin/proglog) - Formalisation of Rushby’s non-interfernce
Homotopy type theory
- Kuratowski-finite sets and finite types in HoTT
- Hedberg’s theorem
- Eckmann-Hilton argument
- Encode-decode method for… (jww Niels van der Weide) The interval, the circle, and set truncation.
Getting useful information from the truncations:
||Σ n, f n = 0|| -> Σ n, f n = 0.See also Auke Booij’s implementation of Escardo’s bounded search and Matthieu Sozeau’s HoTTMarkov.
