Guidi, Ferruccio; Sacerdoti Coen, Claudio, A Survey on Retrieval of Mathematical Knowledge, «MATHEMATICS IN COMPUTER SCIENCE», 2016, 10, pp. 409 - 427 [articolo]
Dunchev, Tsvetan; Sacerdoti Coen, Claudio; Tassi, Enrico, Implementing HOL in an higher order logic programming language, in: ACM International Conference Proceeding Series, New York, NY, USA, Association for Computing Machinery, 2016, 23-, pp. 1 - 10 (atti di: 11th Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2016, Porto, Portugal, 23/06/2016) [Contributo in Atti di convegno]
Guidi, Ferruccio; Sacerdoti Coen, Claudio, A survey on retrieval of mathematical knowledge, in: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Springer Verlag, 2015, 9150, pp. 296 - 315 (atti di: International Conference on Intelligent Computer Mathematics, CICM 2015, Washington DC, USA, July 13-17, 2015) [Contributo in Atti di convegno]
Dunchev, Tsvetan Chavdarov; Guidi, Ferruccio; Sacerdoti Coen, Claudio; Tassi, Enrico, ELPI: Fast, embeddable, λprolog interpreter, in: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Springer Verlag, 2015, 9450, pp. 460 - 468 (atti di: 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2015, Suva, Fiji, November, 24-28, 2015) [Contributo in Atti di convegno]
Tsvetan Chavdarov, Dunchev; Claudio Sacerdoti Coen; Enrico Tassi, Embedded Lambda Prolog Interpreter (ELPI), 2015. [software]
Accattoli, Beniamino; SACERDOTI COEN, Claudio, On the relative usefulness of fireballs, in: 30th Annual ACM/IEEE Symposium on Logic in Computer Science, Institute of Electrical and Electronics Engineers Inc., «PROCEEDINGS - SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE», 2015, pp. 141 - 155 (atti di: 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Grand Prince Hotel, jpn, 2015) [Contributo in Atti di convegno]Open Access
Roberto M. Amadio;Nicolas Ayache;Francois Bobot;Jaap P. Boender;Brian Campbell;Ilias Garnier;Antoine Madet;James McKinna;Dominic P. Mulligan;Mauro Piccolo;Randy Pollack;Yann Régis-Gianas;Claudio Sacerdoti Coen;Ian Stark;Paolo Tranquilli, Certified Complexity (CerCo)Foundational and Practical Aspects of Resource Analysis, in: Lecture Notes in Computer ScienceFoundational and Practical Aspects of Resource Analysis, Springer, «LECTURE NOTES IN COMPUTER SCIENCE», 2014, 8552, pp. 1 - 18 (atti di: Foundational and Practical Aspects of Resource Analysis, Bertinoro, Italy, August 29-31, 2013) [Contributo in Atti di convegno]
Andrea Asperti; Wilmer Ricciotti; Claudio Sacerdoti Coen, Matita Tutorial, «JOURNAL OF FORMALIZED REASONING», 2014, 7, pp. 91 - 199 [articolo]
Boender, J.; Sacerdoti Coen, C., On the correctness of a branch displacement algorithm, in: Tools and Algorithms for the Construction and Analysis of Systems, Berlin, Springer Berlin Heidelberg, «LECTURE NOTES IN COMPUTER SCIENCE», 2014, 8413 LNCS, pp. 605 - 619 (atti di: 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, 5-13/04/2014) [Contributo in Atti di convegno]
Accattoli, B.; Sacerdoti Coen, C., On the value of variables, in: Logic, Language, Information and Computation, Berlin, Springer Berlin Heidelberg, «LECTURE NOTES IN COMPUTER SCIENCE», 2014, 8652 LNCS, pp. 36 - 50 (atti di: 21st Workshop on Logic, Language, Information and Communication, WoLLIC 2014, Valparaiso, Chile, 01-04/09/2014) [Contributo in Atti di convegno]
R. M. Amadio; N. Ayache; Y. Régis-Gianas; R. Saillard; B. Campbell; D. Mulligan; P. Tranquilli; C. Sacerdoti Coen, CerCo Cost Annotating Compiler, 2013. [software]
J. Boender; B. Campbell; I. Gardner; J. McKinna; D. P. Mulligan; M. Piccolo; C. Sacerdoti Coen; I. Stark; P. Tranquilli, Trusted CerCo Cost Annotating Compiler, 2013. [software]
A. Asperti; W. Ricciotti; C. Sacerdoti Coen; E. Tassi, A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions, «LOGICAL METHODS IN COMPUTER SCIENCE», 2012, 8, pp. 1 - 49 [articolo]
O. Al-Hassani; Q. Mahesar; C. Sacerdoti Coen; V. Sorge, A Term Rewriting System for Kuratowski's Closure-Complement Problem, in: Leibniz International Proceedings in Informatics (LIPIcs), DAGSTUHL, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, «LEIBNIZ INTERNATIONAL PROCEEDINGS IN INFORMATICS», 2012, 15, pp. 38 - 52 (atti di: 23rd International Conference on Rewriting Techniques and Applications (RTA'12), Nagoya (Japan), May 30-June 1, 2012) [Contributo in Atti di convegno]
A. Asperti; W. Ricciotti; C. Sacerdoti Coen; E. Tassi, Formal Metatheory of Programming Languages in the Matita Interactive Theorem Prover, «JOURNAL OF AUTOMATED REASONING», 2012, 49(3), pp. 427 - 451 [articolo]
