Adam Chlipala - RankMe

100 papers A* 24A 9B 12C 2Journal 39Unranked 13

Year	Rank	Type	Title / Venue / Authors
2026	B	`conf`	Foundational Verification of Running-Time Bounds for Interactive Programs. CPP Andy Tockman, Pratap Singh, Andres Erbsen, Samuel Gruetter, Adam Chlipala
2026	—	`conf`	On the Common Pitfalls of Designing and Communicating Within-Subjects Experiments in HCI. CHI Extended Abstracts London Bielicke, Emery D. Berger, Adam Chlipala, Eunice Jun
2025	J	`jnl`	Making Concurrent Hardware Verification Sequential. PLDI Thomas Bourgeat, Jiazheng Liu, Adam Chlipala, Arvind
2025	J	`jnl`	PLanet: Formalizing Experimental Design. CoRR London Bielicke, Anna Zhang, Shruti Tyagi, Emery D. Berger, Adam Chlipala, Eunice Jun
2025	J	`jnl`	Pyrosome: Verified Compilation for Modular Metatheory. CoRR Dustin Jamner, Gabriel Kammer, Ritam Nag, Adam Chlipala
2025	J	`jnl`	Pyrosome: Verified Compilation for Modular Metatheory. Proc. ACM Program. Lang. Dustin Jamner, Gabriel Kammer, Ritam Nag, Adam Chlipala
2025	J	`jnl`	Securing Cryptographic Software via Typed Assembly Language (Extended Version). CoRR Shixin Song, Tingzhen Dong, Kosi Nwabueze, Julian Zanders, Andres Erbsen, Adam Chlipala, Mengjia Yan
2025	A*	`conf`	Securing Cryptographic Software via Typed Assembly Language. CCS Shixin Song, Tingzhen Dong, Kosi Nwabueze, Julian Zanders, Andres Erbsen, Adam Chlipala, Mengjia Yan
2025	J	`jnl`	Smooth, Integrated Proofs of Cryptographic Constant Time for Nondeterministic Programs and Compilers. CoRR Owen Conoly, Andres Erbsen, Adam Chlipala
2025	J	`jnl`	Smooth, Integrated Proofs of Cryptographic Constant Time for Nondeterministic Programs and Compilers. Proc. ACM Program. Lang. Owen Conoly, Andres Erbsen, Adam Chlipala
2024	J	`jnl`	A Verified Compiler for a Functional Tensor Language. Proc. ACM Program. Lang. Amanda Liu, Gilbert Bernstein, Adam Chlipala, Jonathan Ragan-Kelley
2024	J	`jnl`	Foundational Integration Verification of a Cryptographic Server. Proc. ACM Program. Lang. Andres Erbsen, Jade Philipoom, Dustin Jamner, Ashley Lin, Samuel Gruetter, Clément Pit-Claudel, Adam Chlipala
2024	J	`jnl`	Live Verification in an Interactive Proof Assistant. Proc. ACM Program. Lang. Samuel Gruetter, Viktor Fukala, Adam Chlipala
2024	A	`conf`	Probability from Possibility: Probabilistic Confidentiality for Storage Systems Under Nondeterminism. CSF Atalay Mert Ileri, Nickolai Zeldovich, Adam Chlipala, M. Frans Kaashoek
2024	A*	`conf`	Specification and Verification of Strong Timing Isolation of Hardware Enclaves. CCS Stella Lau, Thomas Bourgeat, Clément Pit-Claudel, Adam Chlipala
2024	J	`jnl`	Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq. J. Autom. Reason. Jason Gross, Andres Erbsen, Jade Philipoom, Rajashree Agrawal, Adam Chlipala
2024	B	`conf`	Verifying Software Emulation of an Unsupported Hardware Instruction. ITP Samuel Gruetter, Thomas Bourgeat, Adam Chlipala
2023	—	`conf`	CryptOpt: Automatic Optimization of Straightline Code. ICSE Companion Joel Kuepper, David Wu, Andres Erbsen, Jason Gross, Owen Conoly, Chuyue Sun, Samuel Tian, Adam Chlipala, Chitchanok Chuengsatiansup, Daniel Genkin, Markus Wagner, Yuval Yarom
2023	J	`jnl`	CryptOpt: Automatic Optimization of Straightline Code. CoRR Joel Kuepper, Andres Erbsen, Jason Gross, Owen Conoly, Chuyue Sun, Samuel Tian, David Wu, Adam Chlipala, Chitchanok Chuengsatiansup, Daniel Genkin, Markus Wagner, Yuval Yarom
2023	J	`jnl`	CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives. Proc. ACM Program. Lang. Joel Kuepper, Andres Erbsen, Jason Gross, Owen Conoly, Chuyue Sun, Samuel Tian, David Wu, Adam Chlipala, Chitchanok Chuengsatiansup, Daniel Genkin, Markus Wagner, Yuval Yarom
2023	J	`jnl`	Flexible Instruction-Set Semantics via Abstract Monads (Experience Report). Proc. ACM Program. Lang. Thomas Bourgeat, Ian Clester, Andres Erbsen, Samuel Gruetter, Pratap Singh, Andy Wright, Adam Chlipala
2023	J	`jnl`	Omnisemantics: Smooth Handling of Nondeterminism. ACM Trans. Program. Lang. Syst. Arthur Charguéraud, Adam Chlipala, Andres Erbsen, Samuel Gruetter
2023	J	`jnl`	Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq. CoRR Jason Gross, Andres Erbsen, Jade Philipoom, Rajashree Agrawal, Adam Chlipala
2022	B	`conf`	Accelerating Verified-Compiler Development with a Verified Rewriting Engine. ITP Jason Gross, Andres Erbsen, Jade Philipoom, Miraya Poddar-Agrawal, Adam Chlipala
2022	J	`jnl`	Accelerating Verified-Compiler Development with a Verified Rewriting Engine. CoRR Jason Gross, Andres Erbsen, Jade Philipoom, Miraya Poddar-Agrawal, Adam Chlipala
2022	A	`conf`	Adversary Safety by Construction in a Language of Cryptographic Protocols. CSF Timothy M. Braje, Alice R. Lee, Andrew Wagner, Benjamin Kaiser, Daniel Park, Martine Kalke, Robert K. Cunningham, Adam Chlipala
2022	B	`conf`	Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq. ITP Jason Gross, Théo Zimmermann, Miraya Poddar-Agrawal, Adam Chlipala
2022	J	`jnl`	Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq. CoRR Jason Gross, Théo Zimmermann, Miraya Poddar-Agrawal, Adam Chlipala
2022	J	`jnl`	C4: verified transactional objects. Proc. ACM Program. Lang. Mohsen Lesani, Li-yao Xia, Anders Kaseorg, Christian J. Bell, Adam Chlipala, Benjamin C. Pierce, Steve Zdancewic
2022	J	`jnl`	Certifying derivation of state machines from coroutines. Proc. ACM Program. Lang. Mirai Ikebuchi, Andres Erbsen, Adam Chlipala
2022	J	`jnl`	CryptOpt: Verified Compilation with Random Program Search for Cryptographic Primitives. CoRR Joel Kuepper, Andres Erbsen, Jason Gross, Owen Conoly, Chuyue Sun, Samuel Tian, David Wu, Adam Chlipala, Chitchanok Chuengsatiansup, Daniel Genkin, Markus Wagner, Yuval Yarom
2022	—	`conf`	Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols. CAV (2) Joonwon Choi, Adam Chlipala, Arvind
2022	A*	`conf`	Relational compilation for performance-critical applications: extensible proof-producing translation of functional models into low-level code. PLDI Clément Pit-Claudel, Jade Philipoom, Dustin Jamner, Andres Erbsen, Adam Chlipala
2022	J	`jnl`	Verified tensor-program optimization via high-level scheduling rewrites. Proc. ACM Program. Lang. Amanda Liu, Gilbert Louis Bernstein, Adam Chlipala, Jonathan Ragan-Kelley
2021	J	`jnl`	A Multipurpose Formal RISC-V Specification. CoRR Thomas Bourgeat, Ian Clester, Andres Erbsen, Samuel Gruetter, Andrew Wright, Adam Chlipala
2021	A*	`conf`	Effective simulation and debugging for a high-level hardware language using software compilers. ASPLOS Clément Pit-Claudel, Thomas Bourgeat, Stella Lau, Arvind, Adam Chlipala
2021	A*	`conf`	Integration verification across software and hardware for a simple embedded system. PLDI Andres Erbsen, Samuel Gruetter, Joonwon Choi, Clark Wood, Adam Chlipala
2021	J	`jnl`	Skipping the binder bureaucracy with mixed embeddings in a semantics course (functional pearl). Proc. ACM Program. Lang. Adam Chlipala
2020	—	`conf`	Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs. IJCAR (2) Clément Pit-Claudel, Peng Wang, Benjamin Delaware, Jason Gross, Adam Chlipala
2020	B	`conf`	Proof assistants at the hardware-software interface (invited talk). CPP Adam Chlipala
2020	J	`jnl`	Simple High-Level Code For Cryptographic Arithmetic: With Proofs, Without Compromises. ACM SIGOPS Oper. Syst. Rev. Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, Adam Chlipala
2020	A*	`conf`	The essence of Bluespec: a core language for rule-based hardware design. PLDI Thomas Bourgeat, Clément Pit-Claudel, Adam Chlipala, Arvind
2019	J	`jnl`	Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms. J. Autom. Reason. Thomas Grégoire, Adam Chlipala
2019	J	`jnl`	Narcissus: correct-by-construction derivation of decoders and encoders from binary formats. Proc. ACM Program. Lang. Benjamin Delaware, Sorawit Suriyakarn, Clément Pit-Claudel, Qianchuan Ye, Adam Chlipala
2019	A*	`conf`	Simple High-Level Code for Cryptographic Arithmetic - With Proofs, Without Compromises. IEEE Symposium on Security and Privacy Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, Adam Chlipala
2018	J	`jnl`	Computable decision making on the reals and other spaces via partiality and nondeterminism. CoRR Benjamin Sherman, Luke Sciarappa, Adam Chlipala, Michael Carbin
2018	A*	`conf`	Computable decision making on the reals and other spaces: via partiality and nondeterminism. LICS Benjamin Sherman, Luke Sciarappa, Adam Chlipala, Michael Carbin
2018	J	`jnl`	Narcissus: Deriving Correct-By-Construction Decoders and Encoders from Binary Formats. CoRR Sorawit Suriyakarn, Clément Pit-Claudel, Benjamin Delaware, Adam Chlipala
2018	J	`jnl`	Prototyping a functional language using higher-order logic programming: a functional pearl on learning the ways of λProlog/Makam. Proc. ACM Program. Lang. Antonis Stampoulis, Adam Chlipala
2018	A*	`conf`	Proving confidentiality in a file system using DiskSec. OSDI Atalay Mert Ileri, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, Nickolai Zeldovich
2018	B	`conf`	Reification by Parametricity - Fast Setup for Proof by Reflection, in Two Lines of Ltac. ITP Jason Gross, Andres Erbsen, Adam Chlipala
2017	A*	`conf`	A program optimization for automatic database result caching. POPL Ziv Scully, Adam Chlipala
2017	J	`jnl`	Certifying a file system using crash hoare logic: correctness in the presence of crashes. Commun. ACM Tej Chajed, Haogang Chen, Adam Chlipala, M. Frans Kaashoek, Nickolai Zeldovich, Daniel Ziegler
2017	J	`jnl`	Kami: a platform for high-level parametric hardware specification and its modular verification. Proc. ACM Program. Lang. Joonwon Choi, Muralidaran Vijayaraghavan, Benjamin Sherman, Adam Chlipala, Arvind
2017	—	`conf`	The End of History? Using a Proof Assistant to Replace Language Design with Library Design. SNAPL Adam Chlipala, Benjamin Delaware, Samuel Duchovni, Jason Gross, Clément Pit-Claudel, Sorawit Suriyakarn, Peng Wang, Katherine Ye
2017	J	`jnl`	TiML: a functional language for practical complexity analysis with invariants. Proc. ACM Program. Lang. Peng Wang, Di Wang, Adam Chlipala
2017	A*	`conf`	Verifying a high-performance crash-safe file system using a tree specification. SOSP Haogang Chen, Tej Chajed, Alex Konradi, Stephanie Wang, Atalay Mert Ileri, Adam Chlipala, M. Frans Kaashoek, Nickolai Zeldovich
2016	A*	`conf`	Chapar: certified causally consistent distributed key-value stores. POPL Mohsen Lesani, Christian J. Bell, Adam Chlipala
2016	B	`conf`	Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms. ITP Thomas Grégoire, Adam Chlipala
2016	B	`ed.`	Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016 CPP Jeremy Avigad, Adam Chlipala
2016	J	`jnl`	Ur/Web: a simple model for programming the web. Commun. ACM Adam Chlipala
2016	—	`conf`	Using Crash Hoare Logic for Certifying the FSCQ File System. USENIX ATC Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, Nickolai Zeldovich
2015	A	`conf`	An optimizing compiler for a purely functional web-application language. ICFP Adam Chlipala
2015	A*	`conf`	Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant. POPL Benjamin Delaware, Clément Pit-Claudel, Jason Gross, Adam Chlipala
2015	A*	`conf`	From Network Interface to Multithreaded Web Applications: A Case Study in Modular Program Verification. POPL Adam Chlipala
2015	—	`conf`	Modular Deductive Verification of Multiprocessor Hardware Designs. CAV (2) Muralidaran Vijayaraghavan, Adam Chlipala, Arvind, Nirav Dave
2015	—	`conf`	Proof engineering: implementation challenges in rigorously verified software. PLMW@POPL Adam Chlipala
2015	A	`conf`	Specifying Crash Safety for Storage Systems. HotOS Haogang Chen, Daniel Ziegler, Adam Chlipala, M. Frans Kaashoek, Eddie Kohler, Nickolai Zeldovich
2015	A*	`conf`	Ur/Web: A Simple Model for Programming the Web. POPL Adam Chlipala
2015	A*	`conf`	Using Crash Hoare logic for certifying the FSCQ file system. SOSP Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, Nickolai Zeldovich
2014	A	`conf`	Compiler verification meets cross-language linking via data abstraction. OOPSLA Peng Wang, Santiago Cuéllar, Adam Chlipala
2014	B	`conf`	Compositional Computational Reflection. ITP Gregory Malecha, Adam Chlipala, Thomas Braibant
2014	B	`conf`	Experience Implementing a Performant Category-Theory Library in Coq. ITP Jason Gross, Adam Chlipala, David I. Spivak
2014	J	`jnl`	Experience Implementing a Performant Category-Theory Library in Coq. CoRR Jason Gross, Adam Chlipala, David I. Spivak
2014	A*	`conf`	Jitk: A Trustworthy In-Kernel Interpreter Infrastructure. OSDI Xi Wang, David Lazar, Nickolai Zeldovich, Adam Chlipala, Zachary Tatlock
2013	—	`book`	Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant. Adam Chlipala
2013	J	`jnl`	Formal Verification of Hardware Synthesis CoRR Thomas Braibant, Adam Chlipala
2013	A*	`conf`	Formal Verification of Hardware Synthesis. CAV Thomas Braibant, Adam Chlipala
2013	J	`jnl`	MirrorShard: Proof by Computational Reflection with Verified Hints CoRR Gregory Malecha, Adam Chlipala, Thomas Braibant, Patrick Hulin, Edward Z. Yang
2013	A	`conf`	The bedrock structured programming system: combining generative metaprogramming and hoare logic in an extensible program verifier. ICFP Adam Chlipala
2011	A*	`conf`	Mostly-automated verification of low-level programs in computational separation logic. PLDI Adam Chlipala
2010	A*	`conf`	A verified compiler for an impure functional language. POPL Adam Chlipala
2010	J	`jnl`	An Introduction to Programming and Proving with Dependent Types in Coq. J. Formaliz. Reason. Adam Chlipala
2010	—	`conf`	Foundational Program Verification in Coq with Automated Proofs. MSFP@ICFP Adam Chlipala
2010	A*	`conf`	Static Checking of Dynamically-Varying Security Policies in Database-Backed Applications. OSDI Adam Chlipala
2010	A*	`conf`	Ur: statically-typed metaprogramming with type-level record computation. PLDI Adam Chlipala
2009	A	`conf`	Effective interactive proofs for higher-order imperative programs. ICFP Adam Chlipala, J. Gregory Malecha, Greg Morrisett, Avraham Shinnar, Ryan Wisnesky
2008	J	`jnl`	Modular development of certified program verifiers with a proof assistant, . J. Funct. Program. Adam Chlipala
2008	A	`conf`	Parametric higher-order abstract syntax for mechanized semantics. ICFP Adam Chlipala
2007	A*	`conf`	A certified type-preserving compiler from lambda calculus to assembly language. PLDI Adam Chlipala
2006	B	`conf`	A Framework for Certified Program Analysis and Its Applications to Mobile-Code Safety. VMCAI Bor-Yuh Evan Chang, Adam Chlipala, George C. Necula
2006	A	`conf`	Modular development of certified program verifiers with a proof assistant. ICFP Adam Chlipala
2006	—	`conf`	Position Paper: Thoughts on Programming with Proof Assistants. PLPV@IJCAR Adam Chlipala
2005	—	`conf`	Strict bidirectional type checking. TLDI Adam Chlipala, Leaf Petersen, Robert Harper
2005	—	`conf`	The open verifier framework for foundational verifiers. TLDI Bor-Yuh Evan Chang, Adam Chlipala, George C. Necula, Robert R. Schneck
2005	—	`conf`	Type-based verification of assembly language for compiler debugging. TLDI Bor-Yuh Evan Chang, Adam Chlipala, George C. Necula, Robert R. Schneck
2004	A*	`conf`	Generating Tests from Counterexamples. ICSE Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar
2004	C	`conf`	Invited talk: the blast query language for software verification. PEPM Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar
2004	C	`conf`	Invited talk: the blast query language for software verification. PPDP Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar
2004	B	`conf`	The Blast Query Language for Software Verification.. SAS Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar