Adam Chlipala

Available identifiers

zbMath Open chlipala.adam-jWikidataQ102340386 ScholiaQ102340386MaRDI QIDQ1702890

List of research outcomes

Publication	Date of Publication	Type
Towards a scalable proof engine: a performant Prototype rewriting primitive for Coq	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	2022-11-09	Paper
Computable decision making on the reals and other spaces	2021-01-20	Paper
Mostly automated formal verification of loop dependencies with applications to distributed stencil algorithms	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	2017-10-20	Paper
Fiat: deductive synthesis of abstract data types in a proof assistant	2016-09-29	Paper
A verified compiler for an impure functional language	2015-06-11	Paper
Parametric higher-order abstract syntax for mechanized semantics	2015-03-16	Paper
Effective interactive proofs for higher-order imperative programs	2015-01-06	Paper
Experience Implementing a Performant Category-Theory Library in Coq	2014-09-08	Paper
Compositional Computational Reflection	2014-09-08	Paper
https://portal.mardi4nfdi.de/entity/Q5417200	2014-05-16	Paper
https://portal.mardi4nfdi.de/entity/Q3075245	2011-02-10	Paper
Modular development of certified program verifiers with a proof assistant,	2008-12-18	Paper
Verification, Model Checking, and Abstract Interpretation	2007-02-12	Paper
Static Analysis	2005-08-24	Paper

Research outcomes over time

This page was built for person: Adam Chlipala