×

Sacerdoti Coen, Claudio

Author ID: sacerdoti-coen.claudio Recent zbMATH articles by "Sacerdoti Coen, Claudio"
Published as: Sacerdoti Coen, Claudio; Coen, Claudio Sacerdoti; Sacerdoti-Coen, Claudio; Sacerdoti Coen, C.
External Links: ORCID · dblp

Publications by Year

Citations contained in zbMATH Open

45 Publications have been cited 216 times in 123 Documents Cited by Year
The Matita interactive theorem prover. Zbl 1341.68179
Asperti, Andrea; Ricciotti, Wilmer; Sacerdoti Coen, Claudio; Tassi, Enrico
22
2011
User interaction with the Matita proof assistant. Zbl 1132.68673
Asperti, Andrea; Sacerdoti Coen, Claudio; Tassi, Enrico; Zacchiroli, Stefano
17
2007
Hints in unification. Zbl 1252.68246
Asperti, Andrea; Ricciotti, Wilmer; Sacerdoti Coen, Claudio; Tassi, Enrico
12
2009
A content based mathematical search engine: Whelp. Zbl 1172.68623
Asperti, Andrea; Guidi, Ferruccio; Sacerdoti Coen, Claudio; Tassi, Enrico; Zacchiroli, Stefano
12
2006
Crafting a proof assistant. Zbl 1178.68524
Asperti, Andrea; Sacerdoti Coen, Claudio; Tassi, Enrico; Zacchiroli, Stefano
11
2007
Mathematical knowledge management in HELM. Zbl 1025.68080
Asperti, Andrea; Padovani, Luca; Sacerdoti Coen, Claudio; Guidi, Ferruccio; Schena, Irene
11
2003
On the relative usefulness of fireballs. Zbl 1394.68058
Accattoli, Beniamino; Sacerdoti Coen, Claudio
10
2015
ELPI: fast, embeddable, \(\lambda \)Prolog interpreter. Zbl 1471.68046
Dunchev, Cvetan; Guidi, Ferruccio; Sacerdoti Coen, Claudio; Tassi, Enrico
9
2015
Working with mathematical structures in type theory. Zbl 1138.68529
Sacerdoti Coen, Claudio; Tassi, Enrico
8
2008
Tinycals: step by step tacticals. Zbl 1278.68253
Coen, Claudio Sacerdoti; Tassi, Enrico; Zacchiroli, Stefano
8
2007
A constructive and formal proof of Lebesgue’s dominated convergence theorem in the interactive theorem prover Matita. Zbl 1175.68411
Sacerdoti Coen, Claudio; Tassi, Enrico
7
2008
A foundational view on integration problems. Zbl 1278.68289
Rabe, Florian; Kohlhase, Michael; Sacerdoti Coen, Claudio
6
2011
On the value of variables. Zbl 1372.68054
Accattoli, Beniamino; Sacerdoti Coen, Claudio
6
2014
Mathematical libraries as proof assistant environments. Zbl 1108.68601
Sacerdoti Coen, Claudio
5
2004
Spurious disambiguation errors and how to get rid of them. Zbl 1176.68221
Sacerdoti Coen, Claudio; Zacchiroli, Stefano
5
2008
From proof-assistants to distributed libraries of mathematics: Tips and pitfalls. Zbl 1022.68614
Sacerdoti Coen, Claudio
5
2003
A bi-directional refinement algorithm for the calculus of (co)inductive constructions. Zbl 1238.68145
Asperti, Andrea; Ricciotti, Wilmer; Sacerdoti Coen, Claudio; Tassi, Enrico
5
2012
Explanation in natural language of \(\bar\lambda\mu\tilde\mu\)-terms. Zbl 1151.68672
Sacerdoti Coen, Claudio
4
2006
HELM and the semantic math-web. Zbl 1005.68545
Asperti, Andrea; Padovani, Luca; Sacerdoti Coen, Claudio; Schena, Irene
4
2001
A compact kernel for the calculus of inductive constructions. Zbl 1196.68221
Asperti, A.; Ricciotti, W.; Sacerdoti Coen, C.; Tassi, E.
4
2009
A formal correspondence between OMDoc with alternative proofs and the \({\overline{\lambda}\mu\tilde{\mu}}\)-calculus. Zbl 1188.68278
Autexier, Serge; Sacerdoti-Coen, Claudio
3
2006
Efficient ambiguous parsing of mathematical formulae. Zbl 1108.68602
Sacerdoti Coen, Claudio; Zacchiroli, Stefano
3
2004
Certified complexity (CerCo). Zbl 1445.68057
Amadio, Roberto M.; Ayache, Nicolas; Bobot, Francois; Boender, Jaap P.; Campbell, Brian; Garnier, Ilias; Madet, Antoine; McKinna, James; Mulligan, Dominic P.; Piccolo, Mauro; Pollack, Randy; Régis-Gianas, Yann; Sacerdoti Coen, Claudio; Stark, Ian; Tranquilli, Paolo
3
2014
Implementing type theory in higher order constraint logic programming. Zbl 1430.68025
Guidi, Ferruccio; Sacerdoti Coen, Claudio; Tassi, Enrico
3
2019
Relational data across mathematical libraries. Zbl 1428.68352
Condoluci, Andrea; Kohlhase, Michael; Müller, Dennis; Rabe, Florian; Sacerdoti Coen, Claudio; Wenzel, Makarius
3
2019
The Coq library as a theory graph. Zbl 1428.68344
Müller, Dennis; Rabe, Florian; Sacerdoti Coen, Claudio
3
2019
Some considerations on the usability of interactive provers. Zbl 1286.68388
Asperti, Andrea; Sacerdoti Coen, Claudio
3
2010
Formalising overlap algebras in Matita. Zbl 1223.68102
Coen, Claudio Sacerdoti; Tassi, Enrico
2
2011
A semi-reflexive tactic for (sub-)equational reasoning. Zbl 1172.68614
Sacerdoti Coen, Claudio
2
2006
Spurious disambiguation error detection. Zbl 1202.68410
Sacerdoti Coen, Claudio; Zacchiroli, Stefano
2
2007
Intelligent computer mathematics. 12th international conference, CICM 2019, Prague, Czech Republic, July 8–12, 2019. Proceedings. Zbl 1428.68028
2
2019
Matita tutorial. Zbl 1451.68314
Asperti, Andrea; Ricciotti, Wilmer; Coen, Claudio Sacerdoti
2
2014
Nonuniform coercions via unification hints. Zbl 1457.68299
Sacerdoti Coen, Claudio; Tassi, Enrico
2
2011
Formalization of formal topology by means of the interactive theorem prover Matita. Zbl 1335.68223
Asperti, Andrea; Maietti, Maria Emilia; Sacerdoti Coen, Claudio; Sambin, Giovanni; Valentini, Silvio
1
2011
On the value of variables. Zbl 1372.68055
Accattoli, Beniamino; Sacerdoti Coen, Claudio
1
2017
Lebesgue’s dominated convergence theorem in Bishop’s style. Zbl 1251.03089
Sacerdoti Coen, Claudio; Zoli, Enrico
1
2012
Declarative representation of proof terms. Zbl 1185.68633
Sacerdoti Coen, Claudio
1
2010
An interactive algebra course with formalised proofs and definitions. Zbl 1151.97300
Asperti, Andrea; Geuvers, Herman; Loeb, Iris; Mamane, Lionel Elie; Sacerdoti Coen, Claudio
1
2006
A user interface for a mathematical system that allows ambiguous formulae. Zbl 1291.68368
Sacerdoti Coen, Claudio
1
2009
A survey on retrieval of mathematical knowledge. Zbl 1417.68038
Guidi, Ferruccio; Sacerdoti Coen, Claudio
1
2015
A survey on retrieval of mathematical knowledge. Zbl 1409.68085
Guidi, Ferruccio; Sacerdoti Coen, Claudio
1
2016
A plugin to export Coq libraries to XML. Zbl 1428.68345
Sacerdoti Coen, Claudio
1
2019
Reduction and conversion strategies for the calculus of (co)inductive constructions. I. Zbl 1277.68101
Coen, Claudio Sacerdoti
1
2007
Reversibility in Erlang: imperative constructs. Zbl 07615950
Lami, Pietro; Lanese, Ivan; Stefani, Jean-Bernard; Sacerdoti Coen, Claudio; Fabbretti, Giovanni
1
2022
Intelligent computer mathematics. 14th international conference, CICM 2021, Timisoara, Romania, July 26–31, 2021. Proceedings. Zbl 1484.68013
1
2021
Reversibility in Erlang: imperative constructs. Zbl 07615950
Lami, Pietro; Lanese, Ivan; Stefani, Jean-Bernard; Sacerdoti Coen, Claudio; Fabbretti, Giovanni
1
2022
Intelligent computer mathematics. 14th international conference, CICM 2021, Timisoara, Romania, July 26–31, 2021. Proceedings. Zbl 1484.68013
1
2021
Implementing type theory in higher order constraint logic programming. Zbl 1430.68025
Guidi, Ferruccio; Sacerdoti Coen, Claudio; Tassi, Enrico
3
2019
Relational data across mathematical libraries. Zbl 1428.68352
Condoluci, Andrea; Kohlhase, Michael; Müller, Dennis; Rabe, Florian; Sacerdoti Coen, Claudio; Wenzel, Makarius
3
2019
The Coq library as a theory graph. Zbl 1428.68344
Müller, Dennis; Rabe, Florian; Sacerdoti Coen, Claudio
3
2019
Intelligent computer mathematics. 12th international conference, CICM 2019, Prague, Czech Republic, July 8–12, 2019. Proceedings. Zbl 1428.68028
2
2019
A plugin to export Coq libraries to XML. Zbl 1428.68345
Sacerdoti Coen, Claudio
1
2019
On the value of variables. Zbl 1372.68055
Accattoli, Beniamino; Sacerdoti Coen, Claudio
1
2017
A survey on retrieval of mathematical knowledge. Zbl 1409.68085
Guidi, Ferruccio; Sacerdoti Coen, Claudio
1
2016
On the relative usefulness of fireballs. Zbl 1394.68058
Accattoli, Beniamino; Sacerdoti Coen, Claudio
10
2015
ELPI: fast, embeddable, \(\lambda \)Prolog interpreter. Zbl 1471.68046
Dunchev, Cvetan; Guidi, Ferruccio; Sacerdoti Coen, Claudio; Tassi, Enrico
9
2015
A survey on retrieval of mathematical knowledge. Zbl 1417.68038
Guidi, Ferruccio; Sacerdoti Coen, Claudio
1
2015
On the value of variables. Zbl 1372.68054
Accattoli, Beniamino; Sacerdoti Coen, Claudio
6
2014
Certified complexity (CerCo). Zbl 1445.68057
Amadio, Roberto M.; Ayache, Nicolas; Bobot, Francois; Boender, Jaap P.; Campbell, Brian; Garnier, Ilias; Madet, Antoine; McKinna, James; Mulligan, Dominic P.; Piccolo, Mauro; Pollack, Randy; Régis-Gianas, Yann; Sacerdoti Coen, Claudio; Stark, Ian; Tranquilli, Paolo
3
2014
Matita tutorial. Zbl 1451.68314
Asperti, Andrea; Ricciotti, Wilmer; Coen, Claudio Sacerdoti
2
2014
A bi-directional refinement algorithm for the calculus of (co)inductive constructions. Zbl 1238.68145
Asperti, Andrea; Ricciotti, Wilmer; Sacerdoti Coen, Claudio; Tassi, Enrico
5
2012
Lebesgue’s dominated convergence theorem in Bishop’s style. Zbl 1251.03089
Sacerdoti Coen, Claudio; Zoli, Enrico
1
2012
The Matita interactive theorem prover. Zbl 1341.68179
Asperti, Andrea; Ricciotti, Wilmer; Sacerdoti Coen, Claudio; Tassi, Enrico
22
2011
A foundational view on integration problems. Zbl 1278.68289
Rabe, Florian; Kohlhase, Michael; Sacerdoti Coen, Claudio
6
2011
Formalising overlap algebras in Matita. Zbl 1223.68102
Coen, Claudio Sacerdoti; Tassi, Enrico
2
2011
Nonuniform coercions via unification hints. Zbl 1457.68299
Sacerdoti Coen, Claudio; Tassi, Enrico
2
2011
Formalization of formal topology by means of the interactive theorem prover Matita. Zbl 1335.68223
Asperti, Andrea; Maietti, Maria Emilia; Sacerdoti Coen, Claudio; Sambin, Giovanni; Valentini, Silvio
1
2011
Some considerations on the usability of interactive provers. Zbl 1286.68388
Asperti, Andrea; Sacerdoti Coen, Claudio
3
2010
Declarative representation of proof terms. Zbl 1185.68633
Sacerdoti Coen, Claudio
1
2010
Hints in unification. Zbl 1252.68246
Asperti, Andrea; Ricciotti, Wilmer; Sacerdoti Coen, Claudio; Tassi, Enrico
12
2009
A compact kernel for the calculus of inductive constructions. Zbl 1196.68221
Asperti, A.; Ricciotti, W.; Sacerdoti Coen, C.; Tassi, E.
4
2009
A user interface for a mathematical system that allows ambiguous formulae. Zbl 1291.68368
Sacerdoti Coen, Claudio
1
2009
Working with mathematical structures in type theory. Zbl 1138.68529
Sacerdoti Coen, Claudio; Tassi, Enrico
8
2008
A constructive and formal proof of Lebesgue’s dominated convergence theorem in the interactive theorem prover Matita. Zbl 1175.68411
Sacerdoti Coen, Claudio; Tassi, Enrico
7
2008
Spurious disambiguation errors and how to get rid of them. Zbl 1176.68221
Sacerdoti Coen, Claudio; Zacchiroli, Stefano
5
2008
User interaction with the Matita proof assistant. Zbl 1132.68673
Asperti, Andrea; Sacerdoti Coen, Claudio; Tassi, Enrico; Zacchiroli, Stefano
17
2007
Crafting a proof assistant. Zbl 1178.68524
Asperti, Andrea; Sacerdoti Coen, Claudio; Tassi, Enrico; Zacchiroli, Stefano
11
2007
Tinycals: step by step tacticals. Zbl 1278.68253
Coen, Claudio Sacerdoti; Tassi, Enrico; Zacchiroli, Stefano
8
2007
Spurious disambiguation error detection. Zbl 1202.68410
Sacerdoti Coen, Claudio; Zacchiroli, Stefano
2
2007
Reduction and conversion strategies for the calculus of (co)inductive constructions. I. Zbl 1277.68101
Coen, Claudio Sacerdoti
1
2007
A content based mathematical search engine: Whelp. Zbl 1172.68623
Asperti, Andrea; Guidi, Ferruccio; Sacerdoti Coen, Claudio; Tassi, Enrico; Zacchiroli, Stefano
12
2006
Explanation in natural language of \(\bar\lambda\mu\tilde\mu\)-terms. Zbl 1151.68672
Sacerdoti Coen, Claudio
4
2006
A formal correspondence between OMDoc with alternative proofs and the \({\overline{\lambda}\mu\tilde{\mu}}\)-calculus. Zbl 1188.68278
Autexier, Serge; Sacerdoti-Coen, Claudio
3
2006
A semi-reflexive tactic for (sub-)equational reasoning. Zbl 1172.68614
Sacerdoti Coen, Claudio
2
2006
An interactive algebra course with formalised proofs and definitions. Zbl 1151.97300
Asperti, Andrea; Geuvers, Herman; Loeb, Iris; Mamane, Lionel Elie; Sacerdoti Coen, Claudio
1
2006
Mathematical libraries as proof assistant environments. Zbl 1108.68601
Sacerdoti Coen, Claudio
5
2004
Efficient ambiguous parsing of mathematical formulae. Zbl 1108.68602
Sacerdoti Coen, Claudio; Zacchiroli, Stefano
3
2004
Mathematical knowledge management in HELM. Zbl 1025.68080
Asperti, Andrea; Padovani, Luca; Sacerdoti Coen, Claudio; Guidi, Ferruccio; Schena, Irene
11
2003
From proof-assistants to distributed libraries of mathematics: Tips and pitfalls. Zbl 1022.68614
Sacerdoti Coen, Claudio
5
2003
HELM and the semantic math-web. Zbl 1005.68545
Asperti, Andrea; Padovani, Luca; Sacerdoti Coen, Claudio; Schena, Irene
4
2001
all top 5

Cited by 192 Authors

16 Sacerdoti Coen, Claudio
13 Rabe, Florian
11 Asperti, Andrea
11 Kohlhase, Michael
11 Tassi, Enrico
7 Accattoli, Beniamino
6 Ricciotti, Wilmer
4 Guidi, Ferruccio
4 Kaliszyk, Cezary
4 Wenzel, Makarius
3 de Moura, Leonardo
3 Iancu, Mihnea
3 Konovalov, Olexandr
3 Kunčar, Ondřej
3 Miller, Dale Allen
3 Müller, Dennis
3 Popescu, Andrei
3 Roversi, Luca
3 Spitters, Bas
2 Aspinall, David
2 Barras, Bruno
2 Carette, Jacques
2 Charguéraud, Arthur
2 Denney, Ewen
2 Dietrich, Dominik
2 Geuvers, Jan Herman
2 Guerrieri, Giulio
2 Horozal, Fulya
2 Komendantsky, Vladimir
2 Linton, Stephen A.
2 Lüth, Christoph
2 Mahboubi, Assia
2 Maietti, Maria Emilia
2 Maletto, Giacomo
2 O’Connor, Russell
2 Pottier, François
2 Sakaguchi, Kazuhiko
2 Sambin, Giovanni
2 Schulz, Ewaryst
2 Wiedijk, Freek
2 Ziliani, Beta
1 Affeldt, Reynald
1 Allen, Stuart F.
1 Armstrong, Alasdair
1 Avigad, Jeremy
1 Bandyopadhyay, Sivaji
1 Barenbaum, Pablo
1 Berges, Marc
1 Bernardi, Raffaella
1 Betzendahl, Jonas
1 Bickford, Mark
1 Biernacka, Małgorzata
1 Blanchette, Jasmin Christian
1 Blanqui, Frédéric
1 Bocchi, Laura
1 Bonelli, Eduardo
1 Bouzy, Aymeric
1 Buchberger, Bruno
1 Cairns, Paul
1 Caminati, Marco Bright
1 Charatonik, Witold
1 Chen, Xiaoyu
1 Chihani, Zakaria
1 Chugh, Abhishek
1 Cimini, Matteo
1 Cohen, Cyril
1 Cohl, Howard Saul
1 Constable, Robert Lee
1 Crǎciun, Adrian
1 Dadure, Pankaj
1 Dehaye, Paul-Olivier
1 Dreyer, Derek R.
1 Durier, Adrien
1 Eaton, Richard
1 Farka, František
1 Farmer, William M.
1 Filip, Koprivec
1 Fox, Anthony C. J.
1 Fridlender, Daniel
1 Ganesh, Anumanthappa
1 Garillot, François
1 Gauthier, Thibault
1 Ghica, Dan R.
1 Gipp, Bela
1 Gligorić, Miloš V.
1 Gomes, Victor B. F.
1 Gonthier, Georges
1 Govindan, Vediyappan
1 Gow, Jeremy
1 Gunasekaran, Nallappan
1 Hammachukiattikul, Porpattama
1 Hepp, Thomas
1 Heras, Jónathan
1 Hirschkoff, Daniel
1 Honsell, Furio
1 Huffman, Brian
1 Iacob, Alin
1 Jebelean, Tudor
1 Jucovschi, Constantin
1 Kahl, Wolfram
...and 92 more Authors

Citations by Year