Luca Padovani · Università di Torino

ABOUT ME

At least he's handsome

I'm associate professor at the Computer Science Department of the University of Torino and member of the FORMS research group. My research aims at improving the productivity of developers and the quality of software through formal methods. I'm mainly interested in programming languages, type systems and concurrency theory.

TEACHING / DIDATTICAit

Il ricevimento studenti avviene il lunedì dalle 13:00 alle 14:00 (nei periodi di lezione) oppure su appuntamento.

SHORTCUTS

JOURNAL PAPERS

Chaperone Contracts for Higher-Order Sessions
Hernán Melgratti and Luca Padovani
Proceedings of the ACM on Programming Languages 1(ICFP): 1-29, ACM, 2017
Presented at the 22nd ACM SIGPLAN International Conference on Functional Programming (ICFP'17) doi bib pdf artifacts evaluated – reusable & available
On Sessions and Infinite Data
The Chemical Approach to Typestate-Oriented Programming
Silvia Crafa and Luca Padovani
A Core Calculus for Dynamic Delta-Oriented Programming
Ferruccio Damiani, Luca Padovani, Ina Schaefer and Christoph Seidl
A Simple Library Implementation of Binary Sessions
Luca Padovani
Foundations of Session Types and Behavioural Contracts
Hans Hüttel, Ivan Lanese, Vasco T. Vasconcelos, Luís Caires, Marco Carbone, Pierre-Malo Deniélou, Dimitris Mostrous, Luca Padovani, António Ravara, Emilio Tuosto, Hugo Torres Vieira and Gianluigi Zavattaro
ACM Computing Surveys 49(1): 3:1-3:36, ACM, 2016 doi bib pdf
Behavioral Types in Programming Languages
Davide Ancona, Viviana Bono, Mario Bravetti, Joana Campos, Giuseppe Castagna, Pierre-Malo Deniélou, Simon J. Gay, Nils Gesbert, Elena Giachino, Raymond Hu, Einar Broch Johnsen, Francisco Martins, Viviana Mascardi, Fabrizio Montesi, Rumyana Neykova, Nicholas Ng, Luca Padovani, Vasco T. Vasconcelos and Nobuko Yoshida
Fair Subtyping for Multi-Party Session Types
Luca Padovani
Global Progress for Dynamically Interleaved Multiparty Sessions
Type Reconstruction for the Linear π-Calculus with Composite Regular Types
Luca Padovani
An Algebraic Theory for Web Service Contracts
Cosimo Laneve and Luca Padovani
Exception Handling for Copyless Messaging
Svetlana Jakšić and Luca Padovani
On Global Types and Multi-Party Sessions
Typing Copyless Message Passing
Viviana Bono and Luca Padovani
On Projecting Processes into Session Types
Luca Padovani
Contract-Based Discovery of Web Services Modulo Simple Orchestrators
Luca Padovani
PiDuce - A Project for Experimenting Web Services Technologies
Samuele Carpineti, Cosimo Laneve and Luca Padovani
A Theory of Contracts for Web Services
Giuseppe Castagna, Nils Gesbert and Luca Padovani
MathML Formatting with TEX Rules, TEX Fonts, and TEX Quality
Luca Padovani
Mathematical Knowledge Management in HELM
Andrea Asperti, Luca Padovani, Claudio Sacerdoti Coen, Ferruccio Guidi and Irene Schena
Annals of Mathematics and Artificial Intelligence 38(1-3): 27-46, Kluwer Academic Publishers, 2003 doi bib
The GNOME DOM Engine
Paolo Casarini and Luca Padovani

PROCEEDINGS

Context-Free Session Type Inference
Luca Padovani
Proceedings of the 26th European Symposium on Programming (ESOP'17), LNCS 10201: 804-830, ed. Hongseok Yang, Springer, 2017 doi bib pdf html best paper nominee
On Sessions and Infinite Data
Proceedings of the 18th International Conference on Coordination Models and Languages (COORDINATION'16) LNCS 9686: 245-261, eds. Alberto Lluch Lafuente and José Proença, Springer, 2016 doi bib pdf html best paper nominee
The Chemical Approach to Typestate-Oriented Programming
Silvia Crafa and Luca Padovani
Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages & Applications (OOPSLA'15), ACM SIGPLAN Notices 50(10): 917-934, eds. Jonathan Aldrich and Patrick Eugster, ACM, 2015 doi bib pdf
Types for Deadlock-Free Higher-Order Programs
Luca Padovani and Luca Novara
Proceedings of the IFIP International Conference on Formal Methods and Techniques (FORTE'15) LNCS 9039: 3-18, eds. Susanne Graf and Mahesh Viswanathan, Springer, 2015 doi bib
Type Reconstruction Algorithms for Deadlock-Free and Lock-Free Linear π-Calculi
Luca Padovani, Tzu-Chun Chen and Andrea Tosatto
Proceedings of the 17th International Conference on Coordination Models and Languages (COORDINATION'15), LNCS 9037: 83-98, eds. Tom Holvoet and Mirko Viroli, Springer, 2015 doi bib pdf html
Deadlock and Lock Freedom in the Linear π-Calculus
Luca Padovani
Proceedings of the Joint EACSL Annual Conference on Computer Science Logic and Annual ACM/IEEE Symposium on Logic In Computer Science (CSL-LICS'14), pages 72:1-72:10, ACM, 2014 doi bib pdf
Typing Liveness in Multiparty Communicating Systems
Proceedings of the 16th International Conference on Coordination Models and Languages (COORDINATION'14) LNCS 8459: 147-162, eds. Eva Kühn and Rosario Pugliese, Springer, 2014 doi bib pdf html
Session Type Isomorphisms
Proceedings of the Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES'14) EPTCS 155: 61-71, eds. Alastair F. Donaldson and Vasco T. Vasconcelos, Open Publishing Association, 2014 doi bib pdf
Type Reconstruction for the Linear π-Calculus with Composite and Equi-Recursive Types
Luca Padovani
Proceedings of the 17th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'14), LNCS 8412: 88-102, ed. Anca Muscholl, Springer, 2014 doi bib best paper nomineesuperseded
Polymorphic Functions with Set-Theoretic Types - Part 1: Syntax, Semantics, and Evaluation
Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'14) ACM SIGPLAN Notices 49(1): 5-17, ACM, 2014 doi bib
Fair Subtyping for Open Session Types
Luca Padovani
Proceedings of the 40th International Colloquium on Automata, Languages and Programming (ICALP'13), Part II LNCS 7966: 373-384, eds. Fedor V. Fomin, Rūsiņš Freivalds, Marta Kwiatkowska and David Peleg, Springer, 2013 doi bib
An Algebraic Theory for Web Service Contracts
Cosimo Laneve and Luca Padovani
Proceedings of the 10th International Conference on Integrated Formal Methods (IFM'13) LNCS 7940: 301-315, eds. Einar Broch Johnsen and Luigia Petre, Springer, 2013 doi bib invited superseded
Polymorphic Types for Leak Detection in a Session-Oriented Functional Language
Viviana Bono, Luca Padovani and Andrea Tosatto
Proceedings of the IFIP International Conference on Formal Methods and Techniques (FORTE'13) LNCS 7892: 83-98, eds. Dirk Beyer and Michele Boreale, Springer, 2013 doi bib
Inference of Global Progress Properties for Dynamically Interleaved Multiparty Sessions
Proceedings of the 15th International Conference on Coordination Models and Languages (COORDINATION'13) LNCS 7890: 45-59, eds. Christine Julien and Rocco De Nicola, Springer, 2013 doi bib
From Lock Freedom to Progress Using Session Types
Luca Padovani
Proceedings of Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES'13) EPTCS 137: 3-19, eds. Nobuko Yoshida and Wim Vanderbauwhede, Open Publishing Association, 2013 doi bib
Inference of Global Progress Properties for Dynamically Interleaved Multiparty Sessions
Proceedings of the 1st International Workshop on Behavioural Types (BEAT'13), pages 16-27, 2013 bib volume pdf
A Formal Foundation for Dynamic Delta-Oriented Software Product Lines
Ferruccio Damiani, Luca Padovani and Ina Schaefer
Proceedings of the 11th International Conference on Generative Programming and Component Engineering (GPCE'12) ACM SIGPLAN Notices 48(3): 1-10, eds. Klaus Ostermann and Walter Binder, ACM, 2012 doi bib eapls best paper superseded
Exception Handling for Copyless Messaging
Svetlana Jakšić and Luca Padovani
Proceedings of the 14th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP'12), pages 151-162, eds. Danny De Schreye, Gerda Janssens and Andy King, ACM, 2012 doi bib superseded
Polymorphic Endpoint Types for Copyless Message Passing
Viviana Bono and Luca Padovani
Proceedings of the 4th Interaction and Concurrency Experience (ICE'11), EPTCS 59: 52-67, eds. Alexandra Silva, Simon Bliudze, Roberto Bruni and Marco Carbone, Open Publishing Association, 2011 doi bib superseded
Fair Subtyping for Multi-Party Session Types
Luca Padovani
Proceedings of the 13th International Conference on Coordination Models and Languages (COORDINATION'11) LNCS 6721: 127-141, eds. Wolfgang De Meuter and Gruia-Catalin Roman, Springer, 2011 doi bib superseded
On Global Types and Multi-Party Sessions
Proceedings of the IFIP International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS'11), LNCS 6722: 1-28, eds. Roberto Bruni and Juergen Dingel, Springer, 2011 doi bib invited superseded
Typing Copyless Message Passing
Viviana Bono, Chiara Messa and Luca Padovani
Proceedings of the 20th European Symposium on Programming (ESOP'11) LNCS 6602: 57-76, ed. Gilles Barthe, Springer, 2011 doi bib superseded
Session Types = Intersection Types + Union Types
Luca Padovani
Proceedings of the Workshop on Intersection Types and Related Systems (ITRS'10) EPTCS 45: 71-89, eds. Elaine Pimentel, Betti Venneri and Joe Wells, Open Publishing Association, 2011 doi bib
MERCURIO: An Interaction-oriented Framework for Designing, Verifying and Programming Multi-Agent Systems
Proceedings of the 11th International Workshop on Coordination, Organization, Institutions and Norms in Multi-Agent Systems (COIN'10), volume 627: 134-149, eds. Olivier Boissier, Amal El Fallah Seghrouchni, Salima Hassas and Nicolas Maudet, CEUR, 2010 bib pdf volume html
Foundations of Session Types
Giuseppe Castagna, Mariangiola Dezani-Ciancaglini, Elena Giachino and Luca Padovani
Proceedings of the 11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP'09), pages 219-230, eds. António Porto and Francisco J. López-Fraguas, ACM, 2009 doi bib
Contracts for Mobile Processes
Giuseppe Castagna and Luca Padovani
Proceedings of the 20th International Conference on Concurrency Theory (CONCUR'09) LNCS 5710: 211-228, eds. Mario Bravetti and Gianluigi Zavattaro, Springer, 2009 doi bib
Session Types at the Mirror
Luca Padovani
Proceedings of the 2nd Interaction and Concurrency Experience (ICE'09), EPTCS 12: 71-86, eds. Filippo Bonchi, Davide Grohmann, Paola Spoletini and Emilio Tuosto, Open Publishing Association, 2009 doi bib superseded
Contract-Directed Synthesis of Simple Orchestrators
Luca Padovani
Proceedings of the 19th International Conference on Concurrency Theory (CONCUR'08) LNCS 5201: 131-146, eds. Franck van Breugel and Marsha Chechik, Springer, 2008 doi bib superseded
The Pairing of Contracts and Session Types
Cosimo Laneve and Luca Padovani
Concurrency, Graphs and Models (Ugo65'08) LNCS 5065: 681-700, eds. Pierpaolo Degano, Rocco De Nicola and José Meseguer, Springer, 2008 doi bib
A Theory of Contracts for Web Services
Giuseppe Castagna, Nils Gesbert and Luca Padovani
Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'08) ACM SIGPLAN Notices 43(1): 261-272, ACM, 2008 doi bib superseded
The Must Preorder Revisited - An Algebraic Theory for Web Services Contracts
Cosimo Laneve and Luca Padovani
Proceedings of the 18th International Conference on Concurrency Theory (CONCUR'07) LNCS 4703: 212-225, eds. Luís Caires and Vasco T. Vasconcelos, Springer, 2007 doi bib superseded
Performance-Oriented Comparison of Web Services via Client-Specific Testing Preorders
Marco Bernardo and Luca Padovani
Proceedings of the 9th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS'07), LNCS 4468: 269-284, eds. Marcello M. Bonsangue and Einar Broch Johnsen, Springer, 2007 doi bib
A Theory of Contracts for Web Services
Giuseppe Castagna, Nils Gesbert and Luca Padovani
Proceedings of the ACM SIGPLAN Workshop on Programming Language Technologies for XML (PLAN-X'07), pages 37-48, ACM, 2007 bib superseded
A Formal Account of Contracts for Web Services
Samuele Carpineti, Giuseppe Castagna, Cosimo Laneve and Luca Padovani
Proceedings of the 3rd International Workshop on Web Services and Formal Methods (WS-FM'06) LNCS 4184: 148-162, eds. Mario Bravetti, Manuel Núñez and Gianluigi Zavattaro, Springer, 2006 doi bib
From Notation to Semantics: There and Back Again
Luca Padovani and Stefano Zacchiroli
Proceedings of the 5th International Conference on Mathematical Knowledge Management (MKM'06) LNAI 4108: 194-207, eds. Jonathan M. Borwein and William M. Farmer, Springer, 2006 doi bib
Smooth Orchestrators
Cosimo Laneve and Luca Padovani
Proceedings of International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'06), LNCS 3921: 32-46, eds. Luca Aceto and Anna Ingólfsdóttir, Springer, 2006 doi bib
A Distributed Implementation of Mobile Nets as Mobile Agents
Nadia Busi and Luca Padovani
Proceedings of the 7th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS'05), LNCS 3535: 259-274, eds. Martin Steffen and Gianluigi Zavattaro, Springer, 2005 doi bib
Compilation of Generic Regular Path Expressions Using C++ Class Templates
Luca Padovani
Proceedings of the 14th International Conference on Compiler Construction (CC'05) LNCS 3443: 27-42, ed. Rastislav Bodik, Springer, 2005 doi bib
A Generative Approach to the Implementation of Language Bindings for the Document Object Model
Proceedings of the 3rd International Conference on Generative Programming and Component Engineering (GPCE'04) LNCS 3286: 469-487, eds. Gabor Karsai and Eelco Visser, Springer, 2004 doi bib
An Investigation on the Dynamics of Direct-Manipulation Editors for Mathematics
Luca Padovani and Riccardo Solmi
Proceedings of the 3rd International Conference on Mathematical Knowledge Management (MKM'04) LNCS 3119: 302-316, eds. Andrea Asperti, Grzegorz Bancerek and Andrzej Trybulec, Springer, 2004 doi bib
A Math Canvas for the GNOME Desktop
Luca Padovani
Proceedings of the 5th Annual GNOME User and Developer European Conference (GUADEC'04), vol. 107, Agder University College, 2004 bib
Interactive Editing of MathML Markup Using TEX Syntax
Luca Padovani
Proceedings of the International Conference on TeX, XML, and Digital Typography (TUG'04) LNCS 3130: 125-138, eds. Apostolos Syropoulos, Karl Berry, Yannis Haralambous, Baden Hughes, Steven Peter and John Plaice, Springer, 2004 doi bib preprints html
On the Roles of LaTeX and MathML in Encoding and Processing Mathematical Expressions
Luca Padovani
Proceedings of the 2nd International Conference on Mathematical Knowledge Management (MKM'03) LNCS 2594: 66-79, eds. Andrea Asperti, Bruno Buchberger and James H. Davenport, Springer, 2003 doi bib
A Standalone Rendering Engine for MathML
Luca Padovani
Proceedings of the MathML International Conference (MathML'02), pages 109-114, 2002 bib
A Lisp Subset Based on MathML
Yuzhen Xie, Stephen M. Watt and Luca Padovani
Proceedings of the MathML International Conference (MathML'02), pages 101-108, 2002 bib
Mathematical Knowledge Management in HELM
Andrea Asperti, Ferruccio Guidi, Luca Padovani, Claudio Sacerdoti Coen and Irene Schena
Proceedings of the 1st International Conference on Mathematical Knowledge Management (MKM'01), eds. Bruno Buchberger and Olga Caprotti, 2001 pdf
HELM and the Semantic Math-Web
Andrea Asperti, Luca Padovani, Claudio Sacerdoti Coen and Irene Schena
Proceedings of the International Conference on Theorem Proving in Higher Order Logics (TPHOLs'01) LNCS 2152: 59-74, eds. Richard J. Boulton and Paul B. Jackson, Springer, 2001 doi bib superseded
XML, Stylesheets and the Re-mathematization of Formal Content
Andrea Asperti, Luca Padovani, Claudio Sacerdoti Coen and Irene Schena
Proceedings of the Extreme Markup Languages Conference (EXTREME'01), pages 17-27, 2001 bib
The GNOME DOM Engine
Paolo Casarini and Luca Padovani
Proceedings of the Extreme Markup Languages Conference (EXTREME'01), pages 45-53, 2001 bib superseded
Formal Mathematics on the Web
Andrea Asperti, Luca Padovani, Claudio Sacerdoti Coen and Irene Schena
Proceedings of the 8th International Conference on Libraries and Associations in the Transient World: New Technologies and New Forms of Cooperation (Crimea'01), volume 1:342-346, 2001 bib
Formal Mathematics in MathML
Andrea Asperti, Luca Padovani, Claudio Sacerdoti Coen and Irene Schena
Session Presentation at MathML International Conference (MathML'00), 2000 pdf
Towards a Library of Formal Mathematics
Andrea Asperti, Luca Padovani, Claudio Sacerdoti Coen and Irene Schena
Technical Report at International Conference on Theorem Proving in Higher Order Logics (TPHOLs'00), 2000 pdf
Content-Centric Logical Environments
Andrea Asperti, Luca Padovani, Claudio Sacerdoti Coen and Irene Schena
Short Presentation at Annual IEEE Symposium on Logic in Computer Science (LICS'00), 2000 pdf

BOOK CHAPTERS

An OCaml Implementation of Binary Sessions
Hernán Melgratti and Luca Padovani
Behavioural Types: from Theory to Tools, 243-263, eds. Simon J. Gay and António Ravara, River Publishers, 2017 pdf bib book html
Type-Based Analysis of Linear Communications
Luca Padovani
Behavioural Types: from Theory to Tools, 193-217, eds. Simon J. Gay and António Ravara, River Publishers, 2017 pdf bib book html
A Gentle Introduction to Multiparty Asynchronous Session Types
International School on Formal Methods for the Design of Computer, Communication and Software Systems (SFM'15) LNCS 9104: 146-178, eds. Marco Bernardo and Einar Broch Johnsen, Springer, 2015 doi bib
Contract-based Discovery and Adaptation of Web Services
Luca Padovani
International School on Formal Methods for the Design of Computer, Communication and Software Systems (SFM'09) LNCS 5569: 213-260, eds. Marco Bernardo, Luca Padovani and Gianluigi Zavattaro, Springer, 2009 doi bib

EDITED BOOKS

Formal Methods for Web Services, International School on Formal Methods for the Design of Computer, Communication and Software Systems (SFM'09), Advanced Lectures
LNCS 5569, eds. Marco Bernardo, Luca Padovani and Gianluigi Zavattaro, Springer, 2009 doi bib

TECHNICAL REPORTS

Chaperone Contracts for Higher-Order Sessions
Hernán Melgratti and Luca Padovani
Technical Report hal-01545695, 2017 pdf html
On the chemistry of typestate-oriented actors
Silvia Crafa and Luca Padovani
Technical Report CoRR abs/1607.02927, 2016 pdf html
A Simple Library Implementation of Binary Sessions
Luca Padovani
Technical Report hal-01216310, 2015 pdf html superseded
The Chemical Approach to Typestate-Oriented Programming
Silvia Crafa and Luca Padovani
Technical Report hal-01155682, 2015 pdf html
Type Reconstruction Algorithms for Deadlock-Free and Lock-Free Linear π-Calculi
Luca Padovani, Tzu-Chun Chen and Andrea Tosatto
Technical Report hal-01105202, 2015 pdf html
Types for Deadlock-Free Higher-Order Concurrent Programs
Luca Padovani and Luca Novara
Technical Report hal-00954364, 2014 pdf html
Yet Another Type System for Lock-Free Processes
Luca Padovani
Technical Report hal-00863129, 2013 pdf html superseded
Fair Subtyping for Open Session Types
Luca Padovani
Technical Report RT 146/13, Dipartimento di Informatica, University of Torino, 2013
Exception Handling for Copyless Messaging
Svetlana Jakšić and Luca Padovani
Technical Report RT 143/12, Dipartimento di Informatica, University of Torino, 2012 superseded
A Formal Foundation for Dynamic Delta-Oriented Software Product Lines
Ferruccio Damiani, Luca Padovani and Ina Schaefer
Technical Report RT 142/12, Dipartimento di Informatica, University of Torino, 2012
Fair Subtyping for Multi-Party Session Types
Luca Padovani
Technical Report hal-00546531, 2011 pdf html superseded
MERCURIO: An Interaction-oriented Framework for Designing, Verifying and Programming Multi-Agent Systems
Technical Report RT 128/10, Dipartimento di Informatica, University of Torino, 2010 pdf
Stream Processing of XML Documents Made Easy with LALR(1) Parser Generators
Luca Padovani and Stefano Zacchiroli
Technical Report UBLCS-2007-23, Dipartimento di Informatica, Università di Bologna, 2007 pdf
MathML Rendering/Browsing engine
Hanane Naciri and Luca Padovani
Technical Report D4.a, IST-2001-33562 MoWGLI, 2003 pdf
Prototype functionalities for assisted annotation
Philippe Audebaud and Luca Padovani
Technical Report D4.c, IST-2001-33562 MoWGLI, 2003 pdf

SOFTWARE

CobaltBlue: protocol analysis in the Objective Join-Calculus.

FuSe: OCaml library of binary sessions featuring equi-recursive, polymorphic, context-free session types, delegation, subtyping, session type inference.

Hypha: deadlock- and lock-freedom analysis in the linear π-calculus.

RESEARCH PROJECTS

Recent projects

Past projects

EVENTS

SELECTED QUOTES

Home
Produced by an abominable mix of XML, HTML, XSLT, LESS, CSS, Simple Grid, Font Awesome and Alegreya. Inspired by Greg Restall's home page. Last updated Fri, 25 Aug 2017. © Luca Padovani 2017.
Flag Counter