Iliano Cervesato
Associate Teaching Professor of Computer Science
- Interests:
I am interested in the fundamental principles that govern large classes of
problems in computer science in order to exploit their computational
properties to develop algorithms that can effectively solve them. This is
akin to the work of a particle physicist who looks for the fundamental
constituents of our world to develop new processes and materials. Specific
instances encompass:
- Computational logic: logical frameworks, type theory, linear logic, programming languages, logic programming, automated deduction, temporal logic, state, concurrency.
- Computer security: specification languages, cryptographic protocols, intruder models, verification.
- Computer Science education: mobile learing, web-based technology.
- Most recent projects (all projects)
- Most recent papers (all papers)
- The Deductive Spreadsheet (ISBN: 978-3-642-37746-4) , Springer-Verlag, June 2013. Cognitive interface design, Deductive decision-making, End-users, Explanation support, Fixpoints, Graphical user interface, Logic programming, Relational algebra, Spreadsheet paradigm, Usability analysis
- With : Decentralized Execution of Constraint Handling Rules for Ensembles, April 2013. Distributed Programming, Constraint Logic Programming, Multiset Rewritingpapers/cmu-cs-13-106.pdf
- With , : Relating Reasoning Methodologies in Linear Logic and Process Algebra, Electronic Proceedings in Theoretical Computer Science — ETPCS, vol. 101, 50-60, November 2012. Extended version of LINEARITY'12.Linear logic, process algebra, induction, coinduction, contextual preorder, simulation, labeled transition system
- With : Modeling Datalog Fact Assertion and Retraction in Linear Logic, 14th International ACM Symposium on Principles and Practice of Declarative Programming — PPDP'12 (Andy King, editor), 67-78, Leuven, Belgium, 19-21 September 2012. ACM. Datalog, assertion, remotion, truth management, linear logic, correctnesspapers/ppdp12.pdf
- With , , and : Trace Matching in a Concurrent Logical Framework, 7th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice — LFMTP'12 (Adam Chlipala and Carsten Schürmann, editors), Copenhagen, Denmark, 9 September 2012. ACM. CLF, Concurrent traces, epsilon, matchingpapers/lfmtp12.pdf
- An Improved Proof-Theoretic Compilation of Logic Programs, Theory and Practice of Logic Programming — TPLP, vol. 12(4-5) (Agostino Dovier and Vítor Santos Costa, editors), 639-657, Cambridge University Press, 2012. Special Issue on the 28th International Conference on Logic Programming — ICLP'12, Budapest, Hungary, 4-8 September 2012.Compilation; Abstract Logic Programming; Hereditary Harrop Formulas; Well-Moded Logic Programs
- With : Modeling Datalog Fact Assertion and Retraction in Linear Logic, Technical Report CMU-CS-12-126, Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA, August 2012. Datalog, Linear Logic, Retraction, Assertion, Dynamic updatespapers/cmu-cs-12-126.pdf
- With , , and : On Matching in CLF, Technical Report CMU-CS-12-114, Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA, July 2012. CLF, concurrent traces, matching, unification, reasoning about concurrencypapers/cmu-cs-12-114.pdf
- With , , and : On Matching Concurrent Traces, 26th International Workshop on Unification — UNIF'12 (Santiago Escobar, Konstantin Korovin and Vladimir Rybakov, editors), Manchester, UK, 1 July 2012. Matching, parallel computation, computational tracespapers/unif12.pdf
- With , : Relating Reasoning Methodologies in Linear Logic and Process Algebra, Second International Workshop on Linearity — LINEARITY'12 (Sandra Alves and Ian Mackie, editors), Tallinn, Estonia, 1 April 2012. Linear logic, process algebra, induction, coinduction, contextual preorder, simulation, labeled transition systempapers/linearity12.pdf
- Most recent talks (all talks)
- Modeling Datalog Fact Assertion and Retraction in Linear Logic, 14th International ACM Symposium on Principles and Practice of Declarative Programming – PPDP'12, Leuven, Belgium, 20 September 2012. Datalog, assertion, remotion, truth management, linear logic, correctness
- An Improved Proof-Theoretic Compilation of Logic Programs, 28th International Conference on Logic Programming – ICLP'12, Budapest, Hungary, 8 September 2012. Compilation; Abstract Logic Programming; Hereditary Harrop Formulas; Well-Moded Logic Programs
- Contexts for Essay Writing in a Logic Class, The 2012 Communication Symposium at Carnegie Mellon University: Teaching across Cultures and Languages – CS'12, Pittsburgh, PA, 27 June 2012. Essays, typesetting, handwriting
- Relating Reasoning Methodologies in Linear Logic and Process Algebra, Second International Workshop on Linearity – LINEARITY'12, Tallinn, Estonia, 1 April 2012. Linear logic, process algebra, induction, coinduction, contextual preorder, simulation, labeled transition system
- Most recent courses (all courses)
- CS 15-150: Principles of Functional Programming, Carnegie Mellon University (Pittsburgh and Qatar campus), Summer 2013.
- CS 15-199: Discovering Logic, Carnegie Mellon University (Qatar Campus), Spring 2013.
- CS 15-312: Foundations of Programming Languages, Carnegie Mellon University (Qatar Campus), Spring 2013.
- Most recent conferences:
- PPDP'13, 15th International Symposium on Principles and Practice of Declarative Programming – PC member
Madrid, Spain, 16-18 September 2013 (13 June 2013) - SETOP'13, 6th International Workshop on Autonomous and Spontaneous Security – PC member
Egham, UK, 12-13 September 2013 (31 March 2013) - PST'13, 11th Annual Conference on Privacy, Security and Trust – PC member
Terragona, Catalonia, Spain, 10 July 2013 (15 March 2013) - SCSS'13, 5th International Conference on Symbolic Computation in Software Science – PC member
Madrid, Spain, 5-6 July 2013 (10 May 2013) - SAC'13, 28th ACM Symposium on Applied Computing – PC member
Coimbra, Portugal, 18-22 March 2013 (30 August 2012)
- PPDP'13, 15th International Symposium on Principles and Practice of Declarative Programming – PC member
- Curriculum Vitae
- My Erdös number is 3
- My mathematical genealogy goes back to 1380
- In the press:
- ASEE Prism, December 2010 issue: Under attack (cover story), published by the American Society for Engineering Education
- The Piper, 12/10 issue: Classes Find Success with Book-Length Comics
- Akhbar Magazine, Summer/Fall 2010 issue: Discovering Logic with Comics: a new approach to teaching first-year computer science majors
Announcements
- Projects:







