Follow
Adam Chlipala
Adam Chlipala
MIT CSAIL
Verified email at csail.mit.edu - Homepage
Title
Cited by
Cited by
Year
Certified programming with dependent types: a pragmatic introduction to the Coq proof assistant
A Chlipala
MIT Press, 2022
511*2022
Generating tests from counterexamples
D Beyer, AJ Chlipala, TA Henzinger, R Jhala, R Majumdar
Proceedings. 26th International Conference on Software Engineering, 326-335, 2004
3222004
Using Crash Hoare logic for certifying the FSCQ file system
H Chen, D Ziegler, T Chajed, A Chlipala, MF Kaashoek, N Zeldovich
Proceedings of the 25th Symposium on Operating Systems Principles, 18-37, 2015
3152015
Parametric higher-order abstract syntax for mechanized semantics
A Chlipala
Proceedings of the 13th ACM SIGPLAN international conference on Functional …, 2008
2592008
Mostly-automated verification of low-level programs in computational separation logic
A Chlipala
Proceedings of the 32nd ACM SIGPLAN conference on Programming language …, 2011
2122011
A verified compiler for an impure functional language
A Chlipala
ACM Sigplan Notices 45 (1), 93-106, 2010
1602010
A certified type-preserving compiler from lambda calculus to assembly language
A Chlipala
ACM Sigplan Notices 42 (6), 54-65, 2007
1382007
Simple high-level code for cryptographic arithmetic: With proofs, without compromises
A Erbsen, J Philipoom, J Gross, R Sloan, A Chlipala
ACM SIGOPS Operating Systems Review 54 (1), 23-30, 2020
1332020
The Bedrock structured programming system: Combining generative metaprogramming and Hoare logic in an extensible program verifier
A Chlipala
Proceedings of the 18th ACM SIGPLAN international conference on Functional …, 2013
1322013
Kami: a platform for high-level parametric hardware specification and its modular verification
J Choi, M Vijayaraghavan, B Sherman, A Chlipala, Arvind
Proceedings of the ACM on Programming Languages 1 (ICFP), 1-30, 2017
1292017
Effective interactive proofs for higher-order imperative programs
A Chlipala, G Malecha, G Morrisett, A Shinnar, R Wisnesky
ACM Sigplan Notices 44 (9), 79-90, 2009
1272009
Static Checking of {Dynamically-Varying} Security Policies in {Database-Backed} Applications
A Chlipala
9th USENIX Symposium on Operating Systems Design and Implementation (OSDI 10), 2010
1262010
Fiat: Deductive synthesis of abstract data types in a proof assistant
B Delaware, C Pit-Claudel, J Gross, A Chlipala
Acm Sigplan Notices 50 (1), 689-700, 2015
1242015
Ur: statically-typed metaprogramming with type-level record computation
A Chlipala
ACM Sigplan Notices 45 (6), 122-133, 2010
1212010
Ur/Web: A simple model for programming the web
A Chlipala
Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of …, 2015
1102015
Invited talk: the blast query language for software verification
D Beyer, AJ Chlipala, TA Henzinger, R Jhala, R Majumdar
Proceedings of the 2004 ACM SIGPLAN symposium on Partial evaluation and …, 2004
1082004
Chapar: certified causally consistent distributed key-value stores
M Lesani, CJ Bell, A Chlipala
ACM SIGPLAN Notices 51 (1), 357-370, 2016
1062016
Deluge: data dissemination for network reprogramming at scale
A Chlipala, J Hui, G Tolle
University of California, Berkeley, Tech. Rep, 2004
84*2004
Jitk: A Trustworthy {In-Kernel} Interpreter Infrastructure
X Wang, D Lazar, N Zeldovich, A Chlipala, Z Tatlock
11th USENIX Symposium on Operating Systems Design and Implementation (OSDI …, 2014
832014
Verifying a high-performance crash-safe file system using a tree specification
H Chen, T Chajed, A Konradi, S Wang, A İleri, A Chlipala, MF Kaashoek, ...
Proceedings of the 26th Symposium on Operating Systems Principles, 270-286, 2017
792017
The system can't perform the operation now. Try again later.
Articles 1–20