Edit Profile (opens in new tab) Sacerdoti Coen, Claudio Co-Author Distance Author ID: sacerdoti-coen.claudio Published as: Sacerdoti Coen, Claudio; Coen, Claudio Sacerdoti; Sacerdoti-Coen, Claudio; Sacerdoti Coen, C. more...less External Links: ORCID · dblp Documents Indexed: 49 Publications since 2001 4 Contributions as Editor Co-Authors: 52 Co-Authors with 44 Joint Publications 766 Co-Co-Authors all top 5 Co-Authors 9 single-authored 16 Tassi, Enrico 15 Asperti, Andrea 7 Guidi, Ferruccio 7 Zacchiroli, Stefano 6 Ricciotti, Wilmer 4 Rabe, Florian 3 Accattoli, Beniamino 3 Kohlhase, Michael 3 Padovani, Luca 3 Schena, Irene 2 Müller, Dennis 1 Al-Hassani, Osama 1 Amadio, Roberto M. 1 Aspinall, David 1 Autexier, Serge 1 Ayache, Nicolas 1 Bobot, François 1 Boender, Jaap P. 1 Brady, Edwin C. 1 Campbell, Brian 1 Carette, Jacques 1 Condoluci, Andrea 1 Dixon, Lucas 1 Dunchev, Cvetan 1 Fabbretti, Giovanni 1 Garnier, Ilias 1 Geuvers, Jan Herman 1 Kaliszyk, Cezary 1 Kamareddine, Fairouz D. 1 Kohlhase, Andrea 1 Lami, Pietro 1 Lanese, Ivan 1 Loeb, Iris 1 Madet, Antoine 1 Mahesar, Quratul-ain 1 Maietti, Maria Emilia 1 Mamane, Lionel Elie 1 McKinna, James 1 Mulligan, Dominic P. 1 Piccolo, Mauro 1 Pollack, Randy 1 Régis-Gianas, Yann 1 Sambin, Giovanni 1 Schaefer, Jan Frederik 1 Sorge, Volker 1 Stark, Ian 1 Stefani, Jean-Bernard 1 Tranquilli, Paolo 1 Valentini, Silvio 1 Watt, Stephen Michael 1 Wenzel, Makarius 1 Zoli, Enrico all top 5 Serials 3 Journal of Automated Reasoning 3 Lecture Notes in Computer Science 2 MSCS. Mathematical Structures in Computer Science 2 Mathematics in Computer Science 2 Journal of Formalized Reasoning 1 Annals of Pure and Applied Logic 1 Information and Computation 1 Annals of Mathematics and Artificial Intelligence 1 Sādhanā 1 Electronic Notes in Theoretical Computer Science 1 Logical Methods in Computer Science all top 5 Fields 52 Computer science (68-XX) 5 Mathematical logic and foundations (03-XX) 4 General and overarching topics; collections (00-XX) 2 Measure and integration (28-XX) 2 General topology (54-XX) 1 Quantum theory (81-XX) 1 Mathematics education (97-XX) Publications by Year all cited Publications top 5 cited Publications 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 cited Publications top 5 cited Publications 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 all top 5 Cited in 19 Serials 12 Journal of Automated Reasoning 6 Theoretical Computer Science 4 Journal of Functional Programming 4 Mathematics in Computer Science 3 Information and Computation 3 MSCS. Mathematical Structures in Computer Science 3 Journal of Logical and Algebraic Methods in Programming 2 Sādhanā 2 Journal of Applied Logic 2 Logical Methods in Computer Science 1 Journal of Symbolic Computation 1 Formal Aspects of Computing 1 Mathematical Logic Quarterly (MLQ) 1 Annals of Mathematics and Artificial Intelligence 1 The Journal of Logic and Algebraic Programming 1 Theory and Practice of Logic Programming 1 ACM Transactions on Computational Logic 1 Advances in Difference Equations 1 Logica Universalis all top 5 Cited in 15 Fields 117 Computer science (68-XX) 35 Mathematical logic and foundations (03-XX) 3 Category theory; homological algebra (18-XX) 1 General and overarching topics; collections (00-XX) 1 Order, lattices, ordered algebraic structures (06-XX) 1 Number theory (11-XX) 1 Commutative algebra (13-XX) 1 Real functions (26-XX) 1 Special functions (33-XX) 1 Partial differential equations (35-XX) 1 Integral transforms, operational calculus (44-XX) 1 Geometry (51-XX) 1 Numerical analysis (65-XX) 1 Quantum theory (81-XX) 1 Biology and other natural sciences (92-XX) Citations by Year