Experiments in Information Flow Analysis (abstract)

Handling Local State with Global State (abstract)

Certification of Breadth-First Algorithms by Extraction (abstract)

Verified Self-Explaining Computation (abstract)

Self-Certifying Railroad Diagrams, or: How to Teach Nondeterministic Finite Automata (abstract)

How to Calculate with Nondeterministic Functions (abstract)

Setoid Type Theory --- A Syntactic Translation (abstract)

A Calculus for Concurrent and Sequential Programming (abstract)

Cylindric Kleene Lattices for Program Construction (abstract)

A Hierarchy of Monadic Effects for Program Verification Using Equational Reasoning (abstract)

System F in Agda, for Fun and Profit (abstract)

Verified Computations in Mathematical Proofs (abstract)

An Analysis of Repeated Graph Search (abstract)

Shallow Embedding of Type Theory Is Morally Correct (abstract)

The Human in Formal Methods (abstract)

En Garde! Unguarded Iteration for Reversible Computation in the Delay Monad (abstract)

Completeness and Incompleteness of Synchronous Kleene Algebra (abstract)

Unraveling Recursion: Compiling an IR with Recursion to System F (abstract)

Coding with Asymmetric Numeral Systems (abstract)