Introducing the Ur/Web programming language
Excerpts from CPDT
Extended version of my ICFP'06 paper
A Coq framework for verifying that nested loops obey dependency constraints, in message-passing distributed programs that collaboratively fill in the cells of large multidimensional grids
Coq proofs of several distributed key-value store algorithms, including principles for modular reasoning about client programs that use them
A file system implemented and verified in Coq, using separation logic, connected to Linux and providing respectable performance
The whole-program optimizing compiler for Ur/Web
Modular Coq proofs of Bluespec-style hardware descriptions, where processors and memory systems can be verified separately against generic specs (in the style of labeled transition systems) that are compatible with many different optimizations
Deriving efficient OCaml implementations of abstract data types, from declarative specifications, in Coq, mostly automatically. The main case study works with SQL-style relational queries and update operations.
At long last, a paper on the design of Ur/Web, a DSL for Web applications, supporting novel encapsulation techniques and a simple concurrency model for distributed applications
A case study in building a whole-program Coq proof that covers both an application (a database-backed dynamic Web application) and systems infrastructure (a cooperative thread library). The components are verified modularly with Bedrock, and there is a verified compiler for a domain-specific language that can be used to derive similar theorems for similar Web applications, with minimal new proving work.
An approach to verifying multilanguage programs in the Bedrock framework, mixing operational semantics for intralanguage reasoning and axiomatic semantics for interlanguage reasoning
Coq-verified just-in-time compilation for packet filters, etc., in Linux
A framework for combining reflective Coq tactics, applied in the Bedrock system to verify imperative programs
A Coq category-theory library, designed to support computationally efficient proofs of large goals, taking advantage of recent improvements to the homotopy-type-theory Coq version and giving some other wishlist items for Coq
Bedrock takes literally the idea of C as a "macro assembly language." All the programming features are built up as macros on top of assembly language, and macros have verified Hoare logic-style proof rules attached to them, so that one gets a "free" environment for mostly automated deductive program verification for any mix of macros used in a particular program.
A verified compiler for an idealization of the Bluespec hardware description language
A constructive proof that automating separation logic proofs for systems code is easy, despite claims to the contrary coming from SMT solver-centric perspectives. ;-) Specifically, this paper introduced Bedrock, a Coq library for foundational verification of code at the assembly level of abstraction. A mostly-automated separation logic prover uses a modest amount of programmer annotation to drive verification of examples like imperative data structures and a cooperative threading library.
Static analysis for security policies for Ur/Web applications, based on the key new idea of representing policies as SQL queries. The analysis follows the well-trod path of symbolic evaluation and automated first-order-logic theorem-proving.
A first paper about Ur, focusing on the metaprogramming aspect: we can write generic programs that write programs, based on inputs like database schemas, summaries of HTML form configurations, etc., and we can type-check our generators statically without needing to write any proof terms.
A case study in verifying a compiler to an idealized assembly language from an untyped source language with most of the key dynamic features of ML: functions, products, sums, mutable references, and value-carrying exceptions. Syntax is encoded with parametric higher-order abstract syntax (PHOAS), which makes it possible to avoid almost all bookkeeping having to do with binders and fresh name generation. The semantics of the object languages are encoded in a new substitution-free style. All of the proofs are automated with tactic programs that can keep working even after changing the definitions of the languages.
An approach to automating correctness proofs about higher-order, imperative programs in Coq, based on an extensible simplifier for separation logic formulas
A new trick for encoding variable binders in Coq, along with an exploration of its consequences: almost trivial syntax and type-theoretic semantics for languages including such features as polymorphism and complicated binding structure (e.g., ML-style pattern matching); almost trivial type preservation proofs for compiler passes that don't need intensional analysis of variables; mostly-automated semantic correctness proofs about those passes, by way of adding an axiom to make the parametricity of CIC usable explicitly in proofs; and the ability to drop down to more traditional syntactic representations for more arduous but feasible proofs of the same properties, when intensional variable analysis is needed.
A compiler for a tiny statically-typed functional programming language, implemented in Coq with a proof of correctness. The main interesting bits are my use of dependently-typed abstract syntax and denotational semantics, along with some engineering tricks for making the task manageable.
I report on an experience using the Coq proof assistant to develop a program verification tool with a machine-checkable proof of full correctness. The verifier is able to prove memory safety of x86 machine code programs compiled from code that uses algebraic datatypes. The tool's soundness theorem is expressed in terms of the bit-level semantics of x86 programs, so its correctness depends on very few assumptions. I take advantage of Coq's support for programming with dependent types and modules in the structure of my development. The approach is based on developing a library of reusable functors for transforming a verifier at one level of abstraction into a verifier at a lower level. Using this library, it's possible to prototype a verifier based on a new type system with a minimal amount of work, while obtaining a very strong soundness theorem about the final product.
We propose a new technique in support of the construction of efficient Foundational Proof-Carrying Code systems. Instead of suggesting that pieces of mobile code come with proofs of their safety, we instead suggest that they come with executable verifiers that can attest to their safety, as in our previous work on the Open Verifier. However, in contrast to that previous work, here we do away with any runtime proof generation by these verifiers. Instead, we require that the verifier itself is proved sound. To support this, we present a novel technique for extracting proof obligations about ML programs. Using this approach, we are able to demonstrate the first foundational verification technique for Typed Assembly Language with performance comparable to that of the traditional, uncertified TAL type checker.
We describe how to use the BLAST model checker to generate program test suites that achieve full coverage with respect to a given set of predicates.
On verifying functional properties of filesystems in the presence of failures, using proof assistants
Some thoughts on how Coq is actually in pretty good shape to use today for non-trivial programming with dependent types
We show how to combine the interactive proof assistant Coq and the Nelson-Oppen-style automated first-order theorem prover Kettle in a synergistic way. We do this with a Kettle tactic for Coq that uses theory-specific reasoning to simplify goals based on automatically chosen case analyses, returning to the user as subgoals the cases it couldn't prove automatically. The process can then be repeated recursively, using Coq's tactical language as a very expressive extension of the matching strategies found in provers like Simplify. We also discuss how to encode specialized first-order proofs efficiently in Coq using proof by reflection.
We propose a new framework for the construction of trustworthy program verifiers. The Open Verifier architecture can be viewed as an optimized Foundational Proof-Carrying Code toolkit. Instead of proposing that code producers send proofs of safety with all of their programs, we instead suggest that they send re-usable proof-generating verifiers. The proofs are generated in an online fashion via a novel interaction scheme between the untrusted verifier and the trusted core of the system.
A new approach to checking assembly programs in a way similar to that used in the Java Bytecode Verifier. We introduce a novel mixed type/value technique that makes it tractable to deal with some of the "dependent typing" issues that come up. We also present results on using this technique to help students in an undergraduate compilers class debug their class projects.
We present a type system that is useful in saving type annotation space in intermediate language terms expressed in the restricted form called "A-normal form" or "one-half CPS." Our approach imports ideas from strict logic, which is based on the idea of hypotheses that must be used at least once. The resulting system is relevant to the efficiency of type-preserving compilers.
A poster about certified program verifiers in Coq
We describe a system that combines security automaton-based program specification with a facility for relational-style queries about the possible execution paths of a program.
How to do dependently-typed generation of proofs about programming language syntax and semantics
My PhD dissertation, re-presenting the work on certified program verifiers (from ICFP'06) and certified compilers (from PLDI'07)
An overview of a work-in-progress functional programming language that puts dependent types and theorem proving to work to make it easier to write concise and maintainable web applications
This is an extended version of our VMCAI'06 paper, containing a formalization of our model extraction procedure and additional examples.
A summary of my experiences developing a proof-generating TAL type checker within the Open Verifier framework. In the style of Foundational PCC, the soundness of this verifier and the proofs it generates is based on no assumptions about the TAL type system. This was one of the first projects to consider the runtime performance of Foundational PCC-style verification.