: Fast Reflexive Arithmetic Tactics the Linear Case and Beyond.
Nils Anders Danielsson
: A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family.
: Truth Values Algebras and Proof Normalization.
: (In)consistency of Extensions of Higher Order Logic and Type Theory.
: Zermelo's Well-Ordering Theorem in Type Theory.
: Coinductive Correctness of Homographic and Quadratic Algorithms for Exact Real Numbers.
: A Certified Distributed Security Logic for Authorizing Code.