This paper presents Vellvm (verified LLVM), a framework for reasoning about programs
expressed in LLVM's intermediate representation and transformations that operate on it …

Abstract Development of formal proofs of correctness of programs can increase actual and
perceived reliability and facilitate better understanding of program specifications and their …

We present the design and implementation of a typechecker for verifying security properties
of the source code of cryptographic protocols and access control mechanisms. The …

We present parametric higher-order abstract syntax (PHOAS), a new approach to
formalizing the syntax of programming languages in computer proof assistants based on …

This paper provides an introduction to the locally nameless approach to the representation
of syntax with variable binding, focusing in particular on the use of this technique in formal …

Semantic definitions of full-scale programming languages are rarely given, despite the many
potential benefits. Partly this is because the available metalanguages for expressing …

This paper describes a formalisation of the lambda-calculus in a HOL-based theorem prover
using nominal techniques. Central to the formalisation is an inductive set that is bijective with …

Reasoning about the use of external resources is an important aspect of many practical
applications. Effect systems enable tracking such information in types, but at the cost of …

We present a verified compiler to an idealized assembly language from a small, untyped
functional language with mutable references and exceptions. The compiler is programmed …

Q# is a standalone domain-specific programming language from Microsoft for writing and
running quantum programs. Like most industrial languages, it was designed without a formal …