Iliano Cervesato is a computer scientist and Teaching Professor in the Computer Science Department of Carnegie Mellon University (CMU) in Pittsburgh, Pennsylvania. His research spans computational logic, programming languages and computer security, and he has published more than 100 papers in these areas.
With his doctoral advisor Frank Pfenning, Cervesato developed the Linear Logical Framework (LLF), an extension of the LF logical framework with linear types; their 1996 paper introducing it received the LICS Test-of-Time Award in 2016. He later co-developed the Concurrent Logical Framework (CLF) and MSR, a multiset-rewriting formalism for specifying cryptographic protocols, and was a member of the team that in 2005 discovered a man-in-the-middle attack on PKINIT, the public-key extension of the Kerberos authentication protocol. The discovery led the Internet Engineering Task Force (IETF) to change the PKINIT specification and Microsoft to release a security update for several versions of Windows.
Cervesato taught at Carnegie Mellon University in Qatar from 2006 to 2016, where he created Discovering Logic, a first-year course built around the graphic novel Logicomix. Since 2016 he has taught 15-122 Principles of Imperative Computation, a core introductory course in CMU's computer science curriculum, on the Pittsburgh campus. He is also the author of the monograph The Deductive Spreadsheet (Springer, 2013).
Education Cervesato studied computer science at the University of Udine in Italy from 1986, receiving a laurea in Scienze dell'Informazione (computer science) on March 7, 1991. His undergraduate thesis, written in Italian, proposed adding meta-representation capabilities to a logic programming language. From September 1990 he also studied at the University of Houston in Texas, earning a Master of Science in computer science on August 20, 1992, with a thesis on a Warren Abstract Machine implementation of the meta-logic programming language 'Log. His earliest publications, from 1991 to 1993, dealt with 'Log (with Gianfranco Rossi) and with the specification and enforcement of dynamic integrity constraints in databases (with Christoph F. Eick).
Cervesato began doctoral studies in computer science at the University of Turin in November 1991. From April 1994 to November 1995 he was an extended visitor at CMU's Computer Science Department, where he carried out his dissertation research under the supervision of Frank Pfenning. He received his PhD (Dottorato di Ricerca in Informatica) from Turin on October 16, 1996, with the dissertation A Linear Logical Framework. In 1996 he also spent several months visiting the Department of Mathematics at the Technical University of Darmstadt in Germany.
Career Postdoctoral research After completing his doctoral research, Cervesato remained at CMU as a postdoctoral research affiliate in the Computer Science Department until August 1997. From September 1997 to September 1999 he was a postdoctoral research affiliate in the Department of Computer Science at Stanford University. There he worked on the Pleiades project, an Office of Naval Research-funded multi-university research initiative on assurance for modular and mobile code, and co-edited the project's collected reports with John C. Mitchell. While at Stanford he taught a graduate course on linear logic and its applications in the winter quarter of 1999.
Naval Research Laboratory From October 1999 to October 2004, Cervesato was a research scientist with the Advanced Engineering and Sciences Division of ITT Industries, working in support of the Formal Methods Section of the United States Naval Research Laboratory (NRL) in Washington, D.C. At NRL he collaborated with Catherine Meadows and Paul Syverson on the formal analysis of cryptographic protocols. During this period he was also a visiting research collaborator in the Department of Computer Science at Princeton University (2002–2004) and, in July 2003, a visiting fellow in the Department of Computer Engineering at Chulalongkorn University in Bangkok, Thailand. From 1999 to 2004 he took part in a cooperative program on logical methods for the formal verification of software, jointly supported by the National Science Foundation and the Japan Society for the Promotion of Science.
Deductive Solutions, Tulane and George Mason In July 2004 Cervesato founded Deductive Solutions, based in Annandale, Virginia, where he served as chief research scientist. His work on a "deductive spreadsheet" during this period was funded by a DARPA grant (2004–2005). He was a visiting research collaborator in the Department of Mathematics at the University of Pennsylvania from October 2004 to January 2005, a visiting research professor in the Mathematics Department of Tulane University in New Orleans from November 2004 to November 2005, and an adjunct professor in the Department of Information and Software Engineering at George Mason University in the spring of 2006, where he taught a course on secure electronic commerce.
Carnegie Mellon University in Qatar In July 2006 Cervesato joined the computer science teaching faculty of Carnegie Mellon University in Qatar (CMU-Q) in Doha as an associate professor, and was promoted to professor in July 2014. Over the following decade he taught a wide range of courses there (see Teaching) and led or co-led research projects funded by the Qatar National Research Fund (QNRF) and the Qatar Foundation on topics including cryptographic protocol analysis, formal reasoning about languages for distributed computation, programming for large distributed ensembles, hypervisor integrity and automated data inference for end users. According to his curriculum vitae, the grants he has held over his career total about US$7.1 million.
Cervesato organized several international computer science meetings held in Doha. He was program chair of the 12th Asian Computing Science Conference (ASIAN 2007), chair of the security and information assurance track of the 6th ACS/IEEE International Conference on Computer Systems and Applications (AICCSA 2008), co-organizer of the 2nd Annual Doha Conference on Applied Mathematics and Computational Science (2008), and general chair of the 15th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2008). Within CMU-Q he chaired the campus research committee (2009–2010) and the computer science faculty recruitment committee, and maintained the computer science program's website.
Carnegie Mellon University, Pittsburgh In September 2016 Cervesato moved to CMU's Pittsburgh campus as a Teaching Professor in the Computer Science Department. He served on the university's Faculty Senate from 2017 to 2019, and since the fall of 2025 has been the faculty advisor of the development team for Autolab, an autograding platform.
Research Cervesato's research concerns the logical foundations of computation and their application to programming languages, concurrency and security. On his website he compares his approach to that of a particle physicist, who studies the basic constituents of matter in order to develop new processes and materials, describing his aim as identifying the principles that govern large classes of computational problems and using them to derive effective algorithms. His curriculum vitae lists 123 refereed publications written with about 50 co-authors.
Linear logical frameworks A logical framework is a meta-language for representing and reasoning about deductive systems such as logics and programming languages. In his doctoral work with Frank Pfenning, Cervesato designed LLF, a conservative extension of the LF logical framework whose underlying type theory, λΠ⊸&⊤, adds connectives of linear logic to LF's dependent types. Because linear hypotheses must be used exactly once, the framework allows systems involving state to be represented naturally and concisely. The paper introducing LLF, presented at the 1996 Symposium on Logic in Computer Science (LICS) in New Brunswick, New Jersey, illustrated the framework by encoding a version of Mini-ML with references (including its type system, operational semantics and a proof of type preservation) and a sequent calculus for classical linear logic together with its cut-elimination theorem. It also gave LLF an operational reading as a logic programming language. An extended version appeared in Information and Computation in 2002.
In 2016 the LICS 1996 paper received the LICS Test-of-Time Award, which recognizes papers from the symposium twenty years earlier that have proved influential; it shared that year's award with a paper by Parosh Abdulla, Karlis Cerans, Bengt Jonsson and Yih-Kuen Tsay. The award committee described LLF as one of the first logical frameworks to build linearity directly into the framework and the first to do so using an LF-style dependently typed lambda calculus, noting its use in formalizing the metatheory of imperative programming languages and its relevance to newer areas such as quantum programming languages. Later researchers have likewise identified LLF as the first system to combine linear and dependent types, and as the original work in the tradition that keeps linear and unrestricted assumptions in separate contexts.
Cervesato and Pfenning also studied higher-order unification for linear type theories (LICS 1997) and a "spine" representation of linear terms suited to implementation (Journal of Logic and Computation, 2003). With Joshua Hodas and Pfenning, Cervesato developed techniques for efficiently managing linear resources during proof search in linear logic programming languages (Theoretical Computer Science, 2000).
Beginning in 2001, Cervesato, Pfenning, Kevin Watkins and David Walker developed the Concurrent Logical Framework (CLF), which extends LF with linear types for representing state, as in LLF, together with a monad for representing concurrency. CLF was later implemented by Anders Schack-Nielsen and Carsten Schürmann as the Celf system, which has been used to encode examples such as Concurrent ML, the π-calculus, security protocols and Petri nets. Cervesato's subsequent work has addressed meta-reasoning about CLF specifications, such as matching concurrent execution traces (2012), and applications including the formalization of automated trading systems in a concurrent linear framework (2018).
Security protocol analysis At Stanford, Cervesato worked with Nancy Durgin, Patrick Lincoln, John C. Mitchell and Andre Scedrov on MSR, a formalism based on multiset rewriting and linear logic for specifying cryptographic protocols. Their 1999 paper "A Meta-Notation for Protocol Analysis", presented at the 12th IEEE Computer Security Foundations Workshop in Mordano, Italy, used MSR to state the assumptions of the Dolev–Yao model of an intruder. It represented the generation of fresh values such as keys and nonces through existential quantification, and identified a class of theories corresponding to protocols of finite length that may run an unbounded number of instances of each role. The group subsequently related MSR to the strand-space model of protocol analysis (2000; journal version 2005).
Cervesato went on to develop a typed version of MSR with dependent types and subsorting, and published a short LICS 2001 paper titled "The Dolev–Yao Intruder Is the Most Powerful Attacker". He also related MSR to process algebras (with Stefano Bistarelli, Gabriele Lenzini and Fabio Martinelli, 2005) and represented it in an extension of rewriting logic with dependent types (with Mark-Oliver Stehr, 2007). With Paul Syverson he wrote "The Logic of Authentication Protocols", a tutorial chapter based on lectures at the 2000 FOSAD summer school.