×

zbMATH — the first resource for mathematics

Chlipala, Adam J.

Compute Distance To:
Author ID: chlipala.adam-j Recent zbMATH articles by "Chlipala, Adam J."
Published as: Chlipala, Adam; Chlipala, Adam J.
External Links: MGP
Documents Indexed: 18 Publications since 2004, including 1 Book

Publications by Year

Citations contained in zbMATH

15 Publications have been cited 87 times in 74 Documents Cited by Year
Certified programming with dependent types. A pragmatic introduction to the Coq proof assistant. Zbl 1288.68001
Chlipala, Adam
24
2013
Parametric higher-order abstract syntax for mechanized semantics. Zbl 1323.68184
Chlipala, Adam
16
2008
The Blast query language for software verification. Zbl 1104.68408
Beyer, Dirk; Chlipala, Adam J.; Henzinger, Thomas A.; Jhala, Ranjit; Majumdar, Rupak
10
2004
Effective interactive proofs for higher-order imperative programs. Zbl 1302.68087
Chlipala, Adam; Malecha, Gregory; Morrisett, Greg; Shinnar, Avraham; Wisnesky, Ryan
9
2009
Fiat: deductive synthesis of abstract data types in a proof assistant. Zbl 1346.68175
Delaware, Benjamin; Pit-Claudel, Clément; Gross, Jason; Chlipala, Adam
8
2015
A verified compiler for an impure functional language. Zbl 1312.68044
Chlipala, Adam
6
2010
Compositional computational reflection. Zbl 1416.68171
Malecha, Gregory; Chlipala, Adam; Braibant, Thomas
4
2014
An introduction to programming and proving with dependent types in Coq. Zbl 1211.68367
Chlipala, Adam
3
2010
Reification by parametricity – fast setup for proof by reflection, in two lines of Ltac. Zbl 06946986
Gross, Jason; Erbsen, Andres; Chlipala, Adam
1
2018
Mostly automated formal verification of loop dependencies with applications to distributed stencil algorithms. Zbl 06644743
Grégoire, Thomas; Chlipala, Adam
1
2016
Chapar: certified causally consistent distributed key-value stores. Zbl 1347.68117
Lesani, Mohsen; Bell, Christian J.; Chlipala, Adam
1
2016
Modular deductive verification of multiprocessor hardware designs. Zbl 1381.68183
Vijayaraghavan, Muralidaran; Chlipala, Adam; Arvind; Dave, Nirav
1
2015
Experience implementing a performant category-theory library in Coq. Zbl 1416.68163
Gross, Jason; Chlipala, Adam; Spivak, David I.
1
2014
Modular development of certified program verifiers with a proof assistant. Zbl 1155.68429
Chlipala, Adam
1
2008
A framework for certified program analysis and its applications to mobile-code safety. Zbl 1176.68048
Chang, Bor-Yuh Evan; Chlipala, Adam; Necula, George C.
1
2006
Reification by parametricity – fast setup for proof by reflection, in two lines of Ltac. Zbl 06946986
Gross, Jason; Erbsen, Andres; Chlipala, Adam
1
2018
Mostly automated formal verification of loop dependencies with applications to distributed stencil algorithms. Zbl 06644743
Grégoire, Thomas; Chlipala, Adam
1
2016
Chapar: certified causally consistent distributed key-value stores. Zbl 1347.68117
Lesani, Mohsen; Bell, Christian J.; Chlipala, Adam
1
2016
Fiat: deductive synthesis of abstract data types in a proof assistant. Zbl 1346.68175
Delaware, Benjamin; Pit-Claudel, Clément; Gross, Jason; Chlipala, Adam
8
2015
Modular deductive verification of multiprocessor hardware designs. Zbl 1381.68183
Vijayaraghavan, Muralidaran; Chlipala, Adam; Arvind; Dave, Nirav
1
2015
Compositional computational reflection. Zbl 1416.68171
Malecha, Gregory; Chlipala, Adam; Braibant, Thomas
4
2014
Experience implementing a performant category-theory library in Coq. Zbl 1416.68163
Gross, Jason; Chlipala, Adam; Spivak, David I.
1
2014
Certified programming with dependent types. A pragmatic introduction to the Coq proof assistant. Zbl 1288.68001
Chlipala, Adam
24
2013
A verified compiler for an impure functional language. Zbl 1312.68044
Chlipala, Adam
6
2010
An introduction to programming and proving with dependent types in Coq. Zbl 1211.68367
Chlipala, Adam
3
2010
Effective interactive proofs for higher-order imperative programs. Zbl 1302.68087
Chlipala, Adam; Malecha, Gregory; Morrisett, Greg; Shinnar, Avraham; Wisnesky, Ryan
9
2009
Parametric higher-order abstract syntax for mechanized semantics. Zbl 1323.68184
Chlipala, Adam
16
2008
Modular development of certified program verifiers with a proof assistant. Zbl 1155.68429
Chlipala, Adam
1
2008
A framework for certified program analysis and its applications to mobile-code safety. Zbl 1176.68048
Chang, Bor-Yuh Evan; Chlipala, Adam; Necula, George C.
1
2006
The Blast query language for software verification. Zbl 1104.68408
Beyer, Dirk; Chlipala, Adam J.; Henzinger, Thomas A.; Jhala, Ranjit; Majumdar, Rupak
10
2004
all top 5

Cited by 178 Authors

3 Dagand, Pierre-Evariste
3 Malecha, Gregory
3 Myreen, Magnus O.
3 Pientka, Brigitte
2 Avron, Arnon
2 Cohen, Liron
2 Czajka, Łukasz
2 Farmer, William M.
2 Felty, Amy P.
2 Fuchs, Laurent
2 Kaliszyk, Cezary
2 Kumar, Ramana
2 Lammich, Peter
2 Lochbihler, Andreas
2 Momigliano, Alberto
2 Norrish, Michael
2 Popescu, Andrei
2 Reis, Giselle
2 Tabareau, Nicolas
1 Abel, Andreas M.
1 Allais, Guillaume
1 Alpuim, Joao
1 Anand, Abhishek
1 Apt, Krzysztof Rafal
1 Atkey, Robert
1 Axelsson, Emil
1 Balat, Vincent
1 Barone-Adesi, Katerina
1 Barthe, Gilles
1 Bengtson, Jesper
1 Benton, Nick
1 Beringer, Lennart
1 Bernardy, Jean-Philippe
1 Betarte, Gustavo
1 Blanchette, Jasmin Christian
1 Blot, Arthur
1 Boulier, Simon
1 Bouzy, Aymeric
1 Brady, Edwin C.
1 Braghin, Chiara
1 Bubel, Richard
1 Campo, Juan Diego
1 Castegren, Elias
1 Charguéraud, Arthur
1 Charlton, Nathaniel
1 Chaudhuri, Kaustuv
1 Cheney, James
1 Chlipala, Adam J.
1 Chollet, Agathe
1 Christensen, Michael
1 Chuprikov, Pavel
1 Ciaffaglione, Alberto
1 Cohen, Cyril
1 Coquand, Thierry
1 Crole, Roy L.
1 Dabrowski, Frédéric
1 Dams, Dennis René
1 Darais, David
1 Davis, Jared
1 Debbabi, Mourad
1 Drămnesc, Isabela
1 Dreyer, Derek R.
1 Duan, Zhenhua
1 Ekici, Burak
1 Emmi, Michael
1 Ferreira, Francisco H. G.
1 Forster, Yannick
1 Fox, Anthony C. J.
1 Fridlender, Daniel
1 Furniss, Amy
1 Gast, Holger
1 Gheri, Lorenzo
1 Grégoire, Thomas
1 Grumberg, Orna
1 Gu, Ming
1 Guéneau, Armaël
1 Gupta, Rajesh Kumar
1 Haddad, Serge
1 Hähnle, Reiner
1 Hameer, Aliya
1 Hardekopf, Ben
1 Hofmann, Martin
1 Honiden, Shinichi
1 Horsfall, Ben
1 Hur, Chung-Kil
1 Ishikawa, Fuyuki
1 Jebelean, Tudor
1 Jhala, Ranjit
1 Kennedy, Andrew J.
1 Kobayashi, Tsutomu
1 Kohler, Eddie
1 Konnov, Igor V.
1 Krishnaswami, Neelakantan R.
1 Kunze, Fabian
1 Lawall, Julia L.
1 Lazić, Marijana
1 Le Guernic, Paul
1 Li, Li
1 Li, Xiaowei
1 Lima, Leonardo S.
...and 78 more Authors

Citations by Year