Adam Chlipala

Affiliations:
  • MIT, USA


According to our database1, Adam Chlipala authored at least 70 papers between 2004 and 2023.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2023
Flexible Instruction-Set Semantics via Abstract Monads (Experience Report).
Proc. ACM Program. Lang., August, 2023

Omnisemantics: Smooth Handling of Nondeterminism.
ACM Trans. Program. Lang. Syst., March, 2023

CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives.
Proc. ACM Program. Lang., 2023

Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq.
CoRR, 2023

CryptOpt: Automatic Optimization of Straightline Code.
Proceedings of the 45th IEEE/ACM International Conference on Software Engineering: ICSE 2023 Companion Proceedings, 2023

2022
Verified tensor-program optimization via high-level scheduling rewrites.
Proc. ACM Program. Lang., 2022

C4: verified transactional objects.
Proc. ACM Program. Lang., 2022

Certifying derivation of state machines from coroutines.
Proc. ACM Program. Lang., 2022

CryptOpt: Verified Compilation with Random Program Search for Cryptographic Primitives.
CoRR, 2022

Relational compilation for performance-critical applications: extensible proof-producing translation of functional models into low-level code.
Proceedings of the PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13, 2022

Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq.
Proceedings of the 13th International Conference on Interactive Theorem Proving, 2022

Accelerating Verified-Compiler Development with a Verified Rewriting Engine.
Proceedings of the 13th International Conference on Interactive Theorem Proving, 2022

Adversary Safety by Construction in a Language of Cryptographic Protocols.
Proceedings of the 35th IEEE Computer Security Foundations Symposium, 2022

Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols.
Proceedings of the Computer Aided Verification - 34th International Conference, 2022

2021
Skipping the binder bureaucracy with mixed embeddings in a semantics course (functional pearl).
Proc. ACM Program. Lang., 2021

A Multipurpose Formal RISC-V Specification.
CoRR, 2021

Integration verification across software and hardware for a simple embedded system.
Proceedings of the PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021

Effective simulation and debugging for a high-level hardware language using software compilers.
Proceedings of the ASPLOS '21: 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, 2021

2020
Simple High-Level Code For Cryptographic Arithmetic: With Proofs, Without Compromises.
ACM SIGOPS Oper. Syst. Rev., 2020

The essence of Bluespec: a core language for rule-based hardware design.
Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2020

Proof assistants at the hardware-software interface (invited talk).
Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020

Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs.
Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

2019
Narcissus: correct-by-construction derivation of decoders and encoders from binary formats.
Proc. ACM Program. Lang., 2019

Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms.
J. Autom. Reason., 2019

2018
Prototyping a functional language using higher-order logic programming: a functional pearl on learning the ways of λProlog/Makam.
Proc. ACM Program. Lang., 2018

Narcissus: Deriving Correct-By-Construction Decoders and Encoders from Binary Formats.
CoRR, 2018

Proving confidentiality in a file system using DiskSec.
Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation, 2018

Computable decision making on the reals and other spaces: via partiality and nondeterminism.
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018

Reification by Parametricity - Fast Setup for Proof by Reflection, in Two Lines of Ltac.
Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

2017
TiML: a functional language for practical complexity analysis with invariants.
Proc. ACM Program. Lang., 2017

Kami: a platform for high-level parametric hardware specification and its modular verification.
Proc. ACM Program. Lang., 2017

Certifying a file system using crash hoare logic: correctness in the presence of crashes.
Commun. ACM, 2017

Verifying a high-performance crash-safe file system using a tree specification.
Proceedings of the 26th Symposium on Operating Systems Principles, 2017

The End of History? Using a Proof Assistant to Replace Language Design with Library Design.
Proceedings of the 2nd Summit on Advances in Programming Languages, 2017

A program optimization for automatic database result caching.
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

2016
Ur/Web: a simple model for programming the web.
Commun. ACM, 2016

Chapar: certified causally consistent distributed key-value stores.
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

2015
Using Crash Hoare logic for certifying the FSCQ file system.
Proceedings of the 25th Symposium on Operating Systems Principles, 2015

Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant.
Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015

Proof engineering: implementation challenges in rigorously verified software.
Proceedings of the Programming Languages Mentoring Workshop, 2015

From Network Interface to Multithreaded Web Applications: A Case Study in Modular Program Verification.
Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015

An optimizing compiler for a purely functional web-application language.
Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, 2015

Specifying Crash Safety for Storage Systems.
Proceedings of the 15th Workshop on Hot Topics in Operating Systems, 2015

Modular Deductive Verification of Multiprocessor Hardware Designs.
Proceedings of the Computer Aided Verification - 27th International Conference, 2015

2014
Jitk: A Trustworthy In-Kernel Interpreter Infrastructure.
Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation, 2014

Compiler verification meets cross-language linking via data abstraction.
Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications, 2014

Compositional Computational Reflection.
Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

Experience Implementing a Performant Category-Theory Library in Coq.
Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

2013
MirrorShard: Proof by Computational Reflection with Verified Hints
CoRR, 2013

The bedrock structured programming system: combining generative metaprogramming and hoare logic in an extensible program verifier.
Proceedings of the ACM SIGPLAN International Conference on Functional Programming, 2013

Formal Verification of Hardware Synthesis.
Proceedings of the Computer Aided Verification - 25th International Conference, 2013

Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant.
MIT Press, ISBN: 978-0-262-02665-9, 2013

2011
Mostly-automated verification of low-level programs in computational separation logic.
Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, 2011

2010
An Introduction to Programming and Proving with Dependent Types in Coq.
J. Formaliz. Reason., 2010

A verified compiler for an impure functional language.
Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2010

Ur: statically-typed metaprogramming with type-level record computation.
Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2010

Static Checking of Dynamically-Varying Security Policies in Database-Backed Applications.
Proceedings of the 9th USENIX Symposium on Operating Systems Design and Implementation, 2010

Foundational Program Verification in Coq with Automated Proofs.
Proceedings of the 3rd ACM SIGPLAN Workshop on Mathematically Structured Functional Programming, 2010

2009
Effective interactive proofs for higher-order imperative programs.
Proceedings of the Proceeding of the 14th ACM SIGPLAN international conference on Functional programming, 2009

2008
Modular development of certified program verifiers with a proof assistant, .
J. Funct. Program., 2008

Parametric higher-order abstract syntax for mechanized semantics.
Proceedings of the Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, 2008

2007
A certified type-preserving compiler from lambda calculus to assembly language.
Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, 2007

2006
Position Paper: Thoughts on Programming with Proof Assistants.
Proceedings of the Programming Languages meets Program Verification, 2006

A Framework for Certified Program Analysis and Its Applications to Mobile-Code Safety.
Proceedings of the Verification, 2006

2005
Strict bidirectional type checking.
Proceedings of TLDI'05: 2005 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, 2005

Type-based verification of assembly language for compiler debugging.
Proceedings of TLDI'05: 2005 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, 2005

The open verifier framework for foundational verifiers.
Proceedings of TLDI'05: 2005 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, 2005

2004
The Blast Query Language for Software Verification..
Proceedings of the Static Analysis, 11th International Symposium, 2004

Invited talk: the blast query language for software verification.
Proceedings of the 2004 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, 2004

Generating Tests from Counterexamples.
Proceedings of the 26th International Conference on Software Engineering (ICSE 2004), 2004


  Loading...