Publications - Adam Chlipala

Adam Chlipala. An Introduction to Programming and Proving with Dependent Types in Coq. Journal of Formalized Reasoning (JFR). 3(2). 1-93, 2010.

Excerpts from CPDT

Adam Chlipala. Modular Development of Certified Program Verifiers with a Proof Assistant. Journal of Functional Programming (JFP). 18(5/6). 599-647, 2008. Cambridge University Press.

Extended version of my ICFP'06 paper

Adam Chlipala. The Bedrock Structured Programming System: Combining Generative Metaprogramming and Hoare Logic in an Extensible Program Verifier. Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming (ICFP'13). September 2013.

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.

Thomas Braibant, Adam Chlipala. Formal Verification of Hardware Synthesis. Proceedings of the 25th International Conference on Computer Aided Verification (CAV'13). July 2013.

A verified compiler for an idealization of the Bluespec hardware description language

Adam Chlipala. Mostly-Automated Verification of Low-Level Programs in Computational Separation Logic. Proceedings of the ACM SIGPLAN 2011 Conference on Programming Language Design and Implementation (PLDI'11). June 2011.

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.

Adam Chlipala. Static Checking of Dynamically-Varying Security Policies in Database-Backed Applications. Proceedings of the 9th USENIX Symposium on Operating Systems Design and Implementation (OSDI'10). October 2010.

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.

Adam Chlipala. Ur: Statically-Typed Metaprogramming with Type-Level Record Computation. Proceedings of the ACM SIGPLAN 2010 Conference on Programming Language Design and Implementation (PLDI'10). June 2010.

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.

Adam Chlipala. A Verified Compiler for an Impure Functional Language. Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'10). January 2010.

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.

Adam Chlipala, Gregory Malecha, Greg Morrisett, Avraham Shinnar, Ryan Wisnesky. Effective Interactive Proofs for Higher-Order Imperative Programs. Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming (ICFP'09). August 2009.

An approach to automating correctness proofs about higher-order, imperative programs in Coq, based on an extensible simplifier for separation logic formulas

Adam Chlipala. Parametric Higher-Order Abstract Syntax for Mechanized Semantics. Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming (ICFP'08). September 2008.

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.

Adam Chlipala. A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language. Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation (PLDI'07). June 2007.

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.

Adam Chlipala. Modular Development of Certified Program Verifiers with a Proof Assistant. Proceedings of the 11th ACM SIGPLAN International Conference on Functional Programming (ICFP'06). September 2006.

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.

Bor-Yuh Evan Chang, Adam Chlipala, George C. Necula. A Framework for Certified Program Analysis and Its Applications to Mobile-Code Safety. Proceedings of the 7th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'06). January 2006.

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.

Dirk Beyer, Adam J. Chlipala, Thomas Henzinger, Ranjit Jhala, Rupak Majumdar. Generating Tests from Counterexamples. Proceedings of the 26th International Conference on Software Engineering (ICSE'04), IEEE Computer Society Press. May 2004.

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.

Adam Chlipala. Position Paper: Thoughts on Programming with Proof Assistants. Proceedings of the Programming Languages meets Program Verification Workshop (PLPV'06). August 2006.

Some thoughts on how Coq is actually in pretty good shape to use today for non-trivial programming with dependent types

Adam Chlipala, George C. Necula. Cooperative Integration of an Interactive Proof Assistant and an Automated Prover. Proceedings of the 6th International Workshop on Strategies in Automated Deduction (STRATEGIES'06). August 2006.

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.

Bor-Yuh Evan Chang, Adam Chlipala, George C. Necula, Robert R. Schneck. The Open Verifier Framework for Foundational Verifiers. Proceedings of the 2nd ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI'05). January 2005.

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.

Bor-Yuh Evan Chang, Adam Chlipala, George C. Necula, Robert R. Schneck. Type-Based Verification of Assembly Language for Compiler Debugging. Proceedings of the 2nd ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI'05). January 2005.

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.

Adam Chlipala, Leaf Petersen, Robert Harper. Strict Bidirectional Type Checking. Proceedings of the 2nd ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI'05). January 2005.

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.

Adam Chlipala. Developing Certified Program Verifiers with a Proof Assistant. Proceedings of the International Workshop on Proof-Carrying Code (PCC'06). August 2006.

A poster about certified program verifiers in Coq

Dirk Beyer, Adam J. Chlipala, Thomas Henzinger, Ranjit Jhala, Rupak Majumdar. The Blast Query Language for Software Verification. Proceedings of the 11th Static Analysis Symposium (SAS'04), Lecture Notes in Computer Science 3148, Springer-Verlag. August 2004.

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.

Adam Chlipala. Generic Programming and Proving for Programming Language Metatheory. Technical Report UCB/EECS-2007-147. 2007.

How to do dependently-typed generation of proofs about programming language syntax and semantics

Adam Chlipala. Implementing Certified Programming Language Tools in Dependent Type Theory. Technical Report UCB/EECS-2007-113. 2007.

My PhD dissertation, re-presenting the work on certified program verifiers (from ICFP'06) and certified compilers (from PLDI'07)

Adam Chlipala. Scrap Your Web Application Boilerplate, or Metaprogramming with Row Types. Technical Report UCB/EECS-2006-120. 2006.

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

Bor-Yuh Evan Chang, Adam Chlipala, George C. Necula. A Framework for Certified Program Analysis and Its Applications to Mobile-Code Safety. Technical Report UCB/ERL M05/32. UC Berkeley EECS Department. 2005.

This is an extended version of our VMCAI'06 paper, containing a formalization of our model extraction procedure and additional examples.

Adam Chlipala. An Untrusted Verifier for Typed Assembly Language. MS Project Report. Technical Report UCB/ERL M04/41. UC Berkeley EECS Department. 2004.

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.