Adam Chlipala

List of research outcomes

This list is not complete and representing at the moment only items from zbMATH Open and arXiv. We are working on additional sources - please check back here soon!

Publication	Date of Publication	Type
Towards a scalable proof engine: a performant Prototype rewriting primitive for Coq Journal of Automated Reasoning	2024-09-27	Paper
Accelerating verified-compiler development with a verified rewriting engine	2024-07-15	Paper
Automatic test-case reduction in proof assistants: a case study in Coq	2024-07-15	Paper
Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs Automated Reasoning	2022-11-09	Paper
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	2021-01-20	Paper
Mostly automated formal verification of loop dependencies with applications to distributed stencil algorithms Journal of Automated Reasoning	2019-02-18	Paper
Reification by parametricity -- fast setup for proof by reflection, in two lines of \textsc{Ltac}	2018-10-04	Paper
Modular deductive verification of multiprocessor hardware designs	2018-03-01	Paper
A program optimization for automatic database result caching Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages	2017-10-20	Paper
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	2016-09-29	Paper
A verified compiler for an impure functional language Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages	2015-06-11	Paper
Parametric higher-order abstract syntax for mechanized semantics Proceedings of the 13th ACM SIGPLAN international conference on Functional programming	2015-03-16	Paper
Effective interactive proofs for higher-order imperative programs Proceedings of the 14th ACM SIGPLAN international conference on Functional programming	2015-01-06	Paper
Experience implementing a performant category-theory library in Coq Interactive Theorem Proving	2014-09-08	Paper
Compositional computational reflection Interactive Theorem Proving	2014-09-08	Paper
scientific article; zbMATH DE number 6296049 (Why is no real title available?)	2014-05-16	Paper
An introduction to programming and proving with dependent types in Coq	2011-02-10	Paper
Modular development of certified program verifiers with a proof assistant, Journal of Functional Programming	2008-12-18	Paper
Verification, Model Checking, and Abstract Interpretation Lecture Notes in Computer Science	2007-02-12	Paper
Static Analysis Lecture Notes in Computer Science	2005-08-24	Paper

Research outcomes over time

This page was built for person: Adam Chlipala