Hi, I'm Luca Padovani and this is my personal home page.

Publications

2025

• Luca Padovani and Gianluigi Zavattaro, Fair Termination of Asynchronous Binary Sessions, Proceedings of the 39^th European Conference on Object-Oriented Programming (ECOOP’25), 2025.
  long versionpdf

2024

• Ugo Dal Lago and Luca Padovani, On the Almost-Sure Termination of Binary Sessions, Proceedings of the 26^th International Symposium on Principles and Practice of Declarative Programming (PPDP’24), 2024.
  bib slidespdf
• Francesco Dagnino and Luca Padovani, sMALL CaPS: An Infinitary Linear Logic for a Calculus of Pure Sessions, Proceedings of the 26^th International Symposium on Principles and Practice of Declarative Programming (PPDP’24), 2024.
  bib
• Iacopo Colonnelli, Doriana Medić, Alberto Mulone, Viviana Bono, Luca Padovani and Marco Aldinucci, Introducing SWIRL: An Intermediate Representation Language for Scientific Workflows, Proceedings of the 26^th International Symposium on Formal Methods (FM’24), 2024.
  bib long versionpdf
• Ross Horne and Luca Padovani, A Logical Account of Subtyping for Session Types, Journal of Logical and Algebraic Methods in Programming, 2024.
  bib
• Marco Carbone, David Castro-Perez, Francisco Ferreira, Lorenzo Gheri, Frederik Krogsdal Jacobsen, Alberto Momigliano, Luca Padovani, Alceste Scalas, Dawit Tirore, Martin Vassor, Nobuko Yoshida and Daniel Zackon, The Concurrent Calculi Formalisation Benchmark, Proceedings of the 26^th International Conference on Coordination Models and Languages (COORDINATION’24), pages 149-158, 2024.
  abstract bib

  POPLMark and POPLMark Reloaded sparked a flurry of work on machine-checked proofs, and fostered the adoption of proof mechanisation in programming language research. Both challenges were purposely limited in scope, and they do not address concurrency-related issues. We propose a new collection of benchmark challenges focused on the difficulties that typically arise when mechanising formal models of concurrent and distributed programming languages, such as process calculi. Our benchmark challenges address three key topics: linearity, scope extrusion, and coinductive reasoning. The goal of this new benchmark is to clarify, compare, and advance the state of the art, fostering the adoption of proof mechanisation in future research on concurrency.

• Luca Ciccone, Francesco Dagnino and Luca Padovani, Fair Termination of Multiparty Sessions, Journal of Logical and Algebraic Methods in Programming, 2024.
  bib

2023

• Ilaria Castellani, Ornela Dardha, Luca Padovani and Davide Sangiorgi, EXPRESSing Session Types, Proceedings of the Combined 30^th International Workshop on Expressiveness in Concurrency and 20^th Workshop on Structural Operational Semantics (EXPRESS/SOS’23), pages 8-25, 2023.
  bib
• Ross Horne and Luca Padovani, A Logical Account of Subtyping for Session Types, Proceedings of the 14^th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES’23), pages 26-37, 2023.
  bib slidespdf

2022

• Luca Padovani, On the Fair Termination of Client-Server Sessions, Proceedings of the 28^th International Conference on Types for Proofs and Programs (TYPES’22), pages 5:1-5:21, 2022.
  bib slidespdf
• Luca Ciccone and Luca Padovani, An Infinitary Proof Theory of Linear Logic Ensuring Fair Termination in the Linear π-Calculus, Proceedings of the 33^rd International Conference on Concurrency Theory (CONCUR’22), pages 36:1-36:18, 2022.
  bib long versionpdf slidespdf
• Luca Ciccone and Luca Padovani, Inference Systems with Corules for Combined Safety and Liveness Properties of Binary Session Types, Logical Methods in Computer Science, pages 27:1-27:29, 2022.
  bib artifactgit
• Luca Ciccone, Francesco Dagnino and Luca Padovani, Fair Termination of Multiparty Sessions, Proceedings of the 36^th European Conference on Object-Oriented Programming (ECOOP’22), pages 26:1-26:26, 2022.
  bib pdf long versionpdf distinguished paper
• Stephanie Balzer and Luca Padovani, Preface to the special issue on the 12^th workshop on programming language approaches to concurrency and communication-centric software (PLACES) 2020, Journal of Logical and Algebraic Methods in Programming, 2022.
  abstract bib

  This volume contains the JLAMP special issue on the twelfth edition of the workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES 2020). The articles cover topics ranging from the semantics of communicating systems, to static and dynamic analysis techniques for session-based communications, to information flow analysis in heterogeneous organisations.

• Luca Ciccone and Luca Padovani, Fair Termination of Binary Sessions, Proceedings of the ACM on Programming Languages, pages 5:1-5:30, 2022.
  abstract bib preprintpdf long versionpdf artifactgit

  A binary session is a private communication channel that connects two processes, each adhering to a protocol description called session type. In this work, we study the first type system that ensures the fair termination of binary sessions. A session fairly terminates if all of the infinite executions admitted by its protocol are deemed “unrealistic” because they violate certain fairness assumptions. Fair termination entails the eventual completion of all pending input/output actions, including those that depend on the completion of an unbounded number of other actions in possibly different sessions. This form of lock freedom allows us to address a large family of natural communication patterns that fall outside the scope of existing type systems. Our type system is also the first to adopt fair subtyping, a liveness-preserving refinement of the standard subtyping relation for session types that so far has only been studied theoretically. Fair subtyping is surprisingly subtle not only to characterize concisely but also to use appropriately, to the point that the type system must carefully account for all usages of fair subtyping to avoid compromising its liveness-preserving properties.

• Iacopo Colonnelli, Marco Aldinucci, Barbara Cantalupo, Luca Padovani, Sergio Rabellino, Concetto Spampinato, Roberto Morelli, Rosario Di Carlo, Nicolò Magini and Carlo Cavazzoni, Distributed workflows with Jupyter, Future Generation Computer Systems, pages 282-298, 2022.
  abstract bib editor's choice paper in fall 2022

  The designers of a new coordination interface enacting complex workflows have to tackle a dichotomy: choosing a language-independent or language-dependent approach. Language-independent approaches decouple workflow models from the host code’s business logic and advocate portability. Language-dependent approaches foster flexibility and performance by adopting the same host language for business and coordination code. Jupyter Notebooks, with their capability to describe both imperative and declarative code in a unique format, allow taking the best of the two approaches, maintaining a clear separation between application and coordination layers but still providing a unified interface to both aspects. We advocate the Jupyter Notebooks’ potential to express complex distributed workflows, identifying the general requirements for a Jupyter-based Workflow Management System (WMS) and introducing a proof-of-concept portable implementation working on hybrid Cloud-HPC infrastructures. As a byproduct, we extended the vanilla IPython kernel with workflow-based parallel and distributed execution capabilities. The proposed Jupyter-workflow (Jw) system is evaluated on common scenarios for High Performance Computing (HPC) and Cloud, showing its potential in lowering the barriers between prototypical Notebooks and production-ready implementations.

2021

• Luca Ciccone and Luca Padovani, Inference Systems with Corules for Fair Subtyping and Liveness Properties of Binary Session Types, Proceedings of the 48^th International Colloquium on Automata, Languages, and Programming (ICALP’21), pages 125:1-125:16, 2021.
  bib pdf long versionpdf artifactgit

2020

• Luca Ciccone and Luca Padovani, A Dependently Typed Linear π-Calculus in Agda, Proceedings of the 22^nd International Symposium on Principles and Practice of Declarative Programming (PPDP’20), pages 8:1-8:14, 2020.
  bib preprintpdf artifactgit
• Omar Inverso, Hernán Melgratti, Luca Padovani, Catia Trubiani and Emilio Tuosto, Probabilistic Analysis of Binary Sessions, Proceedings of the 31^st International Conference on Concurrency Theory (CONCUR’20), pages 14:1-14:21, 2020.
  bib pdf long versionpdf slidespdf
• Stephanie Balzer and Luca Padovani, Proceedings of the 12^th International Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software, 2020.
  bib

2019

• Rosita Gerbo and Luca Padovani, Concurrent Typestate-Oriented Programming in Java, Proceedings of the 11^th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES’19), pages 24-34, 2019.
  bib pdf slidespdf artifactgit
• Giuseppe Castagna, Mariangiola Dezani-Ciancaglini, Elena Giachino and Luca Padovani, Foundations of Session Types: 10 Years Later, Proceedings of the 21^st International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP’19), pages 1:1-1:3, 2019.
  bib
• Luca Padovani, Context-Free Session Type Inference, ACM Transactions on Programming Languages and Systems, pages 9:1-9:37, 2019.
  bib artifactgit
• Cosimo Laneve and Luca Padovani, Deadlock Analysis of Wait-Notify Coordination, The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy, pages 50-67, 2019.
  bib

2018

• Ugo Liguoro and Luca Padovani, Mailbox Types for Unordered Interactions, Proceedings of the 32^nd European Conference on Object-Oriented Programming (ECOOP’18), pages 15:1-15:28, 2018.
  bib pdf long versionpdf slidespdf artifactgit
• Luca Padovani, A Type Checking Algorithm for Concurrent Object Protocols, Journal of Logical and Algebraic Methods in Programming, pages 16-35, 2018.
  bib
• Luca Padovani, Deadlock-Free Typestate-Oriented Programming, Programming Journal, pages article 15, 2018.
  bib pdf slidespdf
• Ferruccio Damiani, Luca Padovani, Ina Schaefer and Christoph Seidl, A Core Calculus for Dynamic Delta-Oriented Programming, Acta Informatica, pages 269-307, 2018.
• Marco Aldinucci, Luca Padovani and Massimo Torquati, Euro-Par 2018: Parallel Processing, 2018.
  bib

2017

• Silvia Crafa and Luca Padovani, The Chemical Approach to Typestate-Oriented Programming, ACM Transactions on Programming Languages and Systems, pages 13:1-13:45, 2017.
  bib pdf artifactgit
• Hernán Melgratti and Luca Padovani, Chaperone Contracts for Higher-Order Sessions, Proceedings of the ACM on Programming Languages, pages 35:1-35:29, 2017.
  bib long versionpdf slidespdf
• Paula Severi, Luca Padovani, Emilio Tuosto and Mariangiola Dezani-Ciancaglini, On Sessions and Infinite Data, Logical Methods in Computer Science, pages 1-39, 2017.
  bib pdf
• Luca Padovani, A Simple Library Implementation of Binary Sessions, Journal of Functional Programming, 2017.
  bib artifactgit
• Luca Padovani, Context-Free Session Type Inference, Proceedings of the 26^th European Symposium on Programming (ESOP’17), pages 804-830, 2017.
  bib long versionpdf slidespdf artifactgit best paper nomination
• Hernán Melgratti and Luca Padovani, An OCaml Implementation of Binary Sessions, Behavioural Types: from Theory to Tools, pages 243-263, 2017.
  pdf
• Luca Padovani, Type-Based Analysis of Linear Communications, Behavioural Types: from Theory to Tools, pages 193-217, 2017.
  pdf

2016

• 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, Foundations of Session Types and Behavioural Contracts, ACM Computing Surveys, pages 3:1-3:36, 2016.
  bib
• 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, Behavioral Types in Programming Languages, Foundations and Trends in Programming Languages, pages 95-230, 2016.
  bib
• Paula Severi, Luca Padovani, Emilio Tuosto and Mariangiola Dezani-Ciancaglini, On Sessions and Infinite Data, Proceedings of the 18^th International Conference on Coordination Models and Languages (COORDINATION’16), pages 245-261, 2016.
  bib best paper nomination
• Luca Padovani, Fair Subtyping for Multi-Party Session Types, Mathematical Structures in Computer Science, pages 424-464, 2016.
  bib
• Mario Coppo, Mariangiola Dezani-Ciancaglini, Nobuko Yoshida and Luca Padovani, Global Progress for Dynamically Interleaved Multiparty Sessions, Mathematical Structures in Computer Science, pages 238-302, 2016.
  bib

2015

• Silvia Crafa and Luca Padovani, The Chemical Approach to Typestate-Oriented Programming, Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages & Applications (OOPSLA’15), pages 917-934, 2015.
  bib slidespdf artifactgit
• Luca Padovani, Type Reconstruction for the Linear π-Calculus with Composite Regular Types, Logical Methods in Computer Science, pages 1-45, 2015.
  bib long versionpdf
• Luca Padovani and Luca Novara, Types for Deadlock-Free Higher-Order Programs, Proceedings of the IFIP International Conference on Formal Methods and Techniques (FORTE’15), pages 3-18, 2015.
  bib slidespdf
• Luca Padovani, Tzu-Chun Chen and Andrea Tosatto, Type Reconstruction Algorithms for Deadlock-Free and Lock-Free Linear π-Calculi, Proceedings of the 17^th International Conference on Coordination Models and Languages (COORDINATION’15), pages 83-98, 2015.
  bib slidespdf
• Cosimo Laneve and Luca Padovani, An Algebraic Theory for Web Service Contracts, Formal Aspects of Computing, pages 613-640, 2015.
  bib
• Mario Coppo, Mariangiola Dezani-Ciancaglini, Luca Padovani and Nobuko Yoshida, A Gentle Introduction to Multiparty Asynchronous Session Types, International School on Formal Methods for the Design of Computer, Communication and Software Systems (SFM’15), pages 146-178, 2015.
  bib

2014

• Mariangiola Dezani-Ciancaglini, Luca Padovani and Jovanka Pantović, Session Type Isomorphisms, Proceedings of the Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES’14), pages 61-71, 2014.
  abstract bib pdf

  There has been a considerable amount of work on retrieving functions in function libraries using their type as search key. The availability of rich component specifications, in the form of behavioral types, enables similar queries where one can search a component library using the behavioral type of a component as the search key. Just like for function libraries, however, component libraries will contain components whose type differs from the searched one in the order of messages or in the position of the branching points. Thus, it makes sense to also look for those components whose type is different from, but isomorphic to, the searched one.In this article we give semantic and axiomatic characterizations of isomorphic session types. The theory of session type isomorphisms turns out to be subtle. In part this is due to the fact that it relies on a non-standard notion of equivalence between processes. In addition, we do not know whether the axiomatization is complete. It is known that the isomorphisms for arrow, product and sum types are not finitely axiomatisable, but it is not clear yet whether this negative results holds also for the family of types we consider in this work.

• Luca Padovani, Vasco T. Vasconcelos and Hugo Torres Vieira, Typing Liveness in Multiparty Communicating Systems, Proceedings of the 16^th International Conference on Coordination Models and Languages (COORDINATION’14), pages 147-162, 2014.
  abstract bib

  Session type systems are an effective tool to prove that communicating programs do not go wrong, ensuring that the participants of a session follow the protocols described by the types. In a previous work we introduced a typing discipline for the analysis of progress in binary sessions. In this paper we generalize the approach to multiparty sessions following the conversation type approach, while strengthening progress to liveness. We combine the usual session-like fidelity analysis with the liveness analysis and devise an original treatment of recursive types allowing us to address challenging configurations that are out of the reach of existing approaches.

• Luca Padovani, Deadlock and Lock Freedom in the Linear π-Calculus, 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, 2014.
  bib slidespdf artifactgit
• Luca Padovani, Type Reconstruction for the Linear π-Calculus with Composite and Equi-Recursive Types, Proceedings of the 17^th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS’14), pages 88-102, 2014.
  bib slidespdf best paper nomination
• Svetlana Jakšić and Luca Padovani, Exception Handling for Copyless Messaging, Science of Computer Programming, pages 22-51, 2014.
  abstract bib

  Copyless messaging is a communication paradigm in which only pointers to messages are exchanged between sender and receiver processes. Because of its intrinsically low overhead, copyless messaging is suitable for the efficient implementation of communication-intensive software systems where processes have access to a shared address space. Unfortunately, the very nature of the paradigm fosters the proliferation of programming errors due to the explicit use of pointers and to the sharing of data. In this paper we study a type discipline for copyless messaging that, together with some minimal support from the runtime system, is able to guarantee the absence of communication errors, memory faults, and memory leaks in the presence of exceptions. To formalize the semantics of processes we draw inspiration from software transactional memories: in our case a transaction is a process that is meant to accomplish some exchange of messages and that should either be executed completely, or should have no observable effect if aborted by an exception.

• Giuseppe Castagna, Kim Nguyễn, Zhiwu Xu, Hyeonseung Im, Sergueı̈ Lenglet and Luca Padovani, Polymorphic Functions with Set-Theoretic Types - Part 1: Syntax, Semantics, and Evaluation, Proceedings of the 41^st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’14), pages 5-17, 2014.
  bib

2013

• Luca Padovani, From Lock Freedom to Progress Using Session Types, Proceedings of Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES’13), pages 3-19, 2013.
  abstract bib slidespdf

  Inspired by Kobayashi’s type system for lock freedom, we define a behavioral type system for ensuring progress in a language of binary sessions. The key idea is to annotate actions in session types with priorities representing the urgency with which such actions must be performed and to verify that processes perform such actions with the required priority. Compared to related systems for session-based languages, the presented type system is relatively simpler and establishes progress for a wider range of processes.

• Luca Padovani, Fair Subtyping for Open Session Types, Proceedings of the 40^th International Colloquium on Automata, Languages and Programming (ICALP’13), Part II, pages 373-384, 2013.
  bib long versionpdf slidespdf
• Mario Coppo, Mariangiola Dezani-Ciancaglini, Luca Padovani and Nobuko Yoshida, Inference of Global Progress Properties for Dynamically Interleaved Multiparty Sessions, Proceedings of the 15^th International Conference on Coordination Models and Languages (COORDINATION’13), pages 45-59, 2013.
  bib slidespdf
• Mario Coppo, Mariangiola Dezani-Ciancaglini, Luca Padovani and Nobuko Yoshida, Inference of Global Progress Properties for Dynamically Interleaved Multiparty Sessions, Proceedings of the 1^st International Workshop on Behavioural Types (BEAT’13), pages 16-27, 2013.
  abstract slidespdf

  A multiparty session forms a unit of structured interactions among several processes which follow a specified protocol described as a global type. Well-known communication-oriented type systems guarantee communication safety and progress within single sessions, but do not take into account the dependencies arising from the interleaving of simultaneously active sessions and from session delegations. As a consequence, a system of well-typed processes may fail to have progress, even assuming that helper processes can join the system after its execution has started. In this paper we develop a static analysis technique, specified as a set of syntax-directed inference rules, that is capable of verifying whether a system of processes engaged in simultaneously active multiparty sessions has the progress property.

• Viviana Bono, Luca Padovani and Andrea Tosatto, Polymorphic Types for Leak Detection in a Session-Oriented Functional Language, Proceedings of the IFIP International Conference on Formal Methods and Techniques (FORTE’13), pages 83-98, 2013.
  abstract bib

  Copyless message passing is a communication paradigm in which only pointers are exchanged between sender and receiver processes. Because of its nature, this paradigm requires that messages are treated as linear resources. Yet, even linear type systems leave room for scenarios where apparently well-typed programs may leak memory. In this work we develop a polymorphic type system for leak-free copyless messaging in a functional setting, where first-class functions can be used as messages.

• Cosimo Laneve and Luca Padovani, An Algebraic Theory for Web Service Contracts, Proceedings of the 10^th International Conference on Integrated Formal Methods (IFM’13), pages 301-315, 2013.
  abstract bib

  We study a natural notion of compliance between clients and services in terms of their BPEL (abstract) descriptions. The induced preorder shows interesting connections with the must preorder and has normal form representatives that are parallel-free finite-state activities, called contracts. The preorder also admits the notion of least service contract that is compliant with a client contract, called principal dual contract. Our framework serves as a foundation of Web service technologies for connecting abstract and concrete service definitions and for service discovery.

2012

• Giuseppe Castagna, Mariangiola Dezani-Ciancaglini and Luca Padovani, On Global Types and Multi-Party Sessions, Logical Methods in Computer Science, pages 1-45, 2012.
  bib
• Luca Padovani, On Projecting Processes into Session Types, Mathematical Structures in Computer Science, pages 237-289, 2012.
  abstract bib

  We define session types as projections of the behavior of processes with respect to the operations processes perform on channels. This calls for a parallel composition operator over session types denoting the simultaneous access to a channel by two or more processes. The proposed approach allows us to define a semantically grounded theory of session types that does not require the linear usage of channels. However, type preservation and progress can only be guaranteed for processes that never receive channels they already own. A number of examples show that the resulting framework validates existing session type theories and unifies them to some extent.

• Ferruccio Damiani, Luca Padovani and Ina Schaefer, A Formal Foundation for Dynamic Delta-Oriented Software Product Lines, Proceedings of the 11^th International Conference on Generative Programming and Component Engineering (GPCE’12), pages 1-10, 2012.
  abstract bib eapls best paper

  Delta-oriented programming (DOP) is a flexible approach for implementing software product lines (SPLs). Delta-oriented SPLs are implemented by a code base (a set of delta modules encapsulating changes to object-oriented programs) and a product line declaration (providing the connection of the delta modules with the product features). In this paper, we extend DOP by the capability to switch the implemented product configuration at runtime and present a formal foundation for dynamic DOP. A dynamic DOP SPL is a DOP SPL with a dynamic reconfiguration graph that specifies how to switch between different feature configurations. Dynamic DOP supports (unanticipated) software evolution such that at runtime, the product line declaration, the code base and the dynamic reconfiguration graph can be changed in any (unanticipated) way that preserves the currently running product. The type system of our dynamic DOP core calculus ensures that the dynamic reconfigurations lead to type safe products and do not cause runtime type errors.

• Svetlana Jakšić and Luca Padovani, Exception Handling for Copyless Messaging, Proceedings of the 14^th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP’12), pages 151-162, 2012.
  abstract bib slidespdf

  Copyless messaging is a communication mechanism in which only pointers to messages are exchanged between sender and receiver processes. Because of its intrinsically low overhead, copyless messaging can be profitably adopted for the development of complex software systems where processes have access to a shared address space. However, the very same mechanism fosters the proliferation of programming errors due to the explicit use of pointers and to the sharing of data. In this paper we study a type discipline for copyless messaging that, together with some minimal support from the runtime system, is able to guarantee the absence of communication errors, memory faults, and memory leaks in presence of exceptions. To formalize the semantics of processes we draw inspiration from software transactional memories: in our case a transaction is a process that is meant to accomplish some exchange of messages and that should either be executed completely, or should have no observable effect if aborted by an exception.

• Viviana Bono and Luca Padovani, Typing Copyless Message Passing, Logical Methods in Computer Science, pages 1-50, 2012.
  abstract bib pdf

  We present a calculus that models a form of process interaction based on copyless message passing, in the style of Singularity OS. The calculus is equipped with a type system ensuring that well-typed processes are free from memory faults, memory leaks, and communication errors. The type system is essentially linear, but we show that linearity alone is inadequate, because it leaves room for scenarios where well-typed processes leak significant amounts of memory. We address these problems basing the type system upon an original variant of session types.

2011

• Giuseppe Castagna, Mariangiola Dezani-Ciancaglini and Luca Padovani, On Global Types and Multi-Party Sessions, Proceedings of the IFIP International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS’11), pages 1-28, 2011.
  abstract bib

  We present a new, streamlined language of global types equipped with a trace-based semantics and whose features and restrictions are semantically justified. The multi-party sessions obtained projecting our global types enjoy a liveness property in addition to the traditional progress and are shown to be sound and complete with respect to the set of traces of the originating global type. Our notion of completeness is less demanding than the classical ones, allowing a multi-party session to leave out redundant traces from an underspecified global type.

• Luca Padovani, Session Types = Intersection Types + Union Types, Proceedings of the Workshop on Intersection Types and Related Systems (ITRS’10), pages 71-89, 2011.
  abstract bib slidespdf

  We propose a semantically grounded theory of session types which relies on intersection and union types. We argue that intersection and union types are natural candidates for modeling branching points in session types and we show that the resulting theory overcomes some important defects of related behavioral theories. In particular, intersections and unions provide a native solution to the problem of computing joins and meets of session types. Also, the subtyping relation turns out to be a pre-congruence, while this is not always the case in related behavioral theories.

• Luca Padovani, Fair Subtyping for Multi-Party Session Types, Proceedings of the 13^th International Conference on Coordination Models and Languages (COORDINATION’11), pages 127-141, 2011.
  abstract bib slidespdf

  The standard subtyping relation used in dyadic session type theories may compromise the liveness of multi-party sessions. In this paper we define a fair subtyping relation for multi-party session types that preserves liveness, we relate it with the standard subtyping relation, and we give algorithms for deciding it. As a side effect, we provide an original and remarkably simple coinductive characterization of the fair testing preorder for nondeterministic, sequential processes consisting of internal choices of outputs and external choices of inputs.

• Viviana Bono and Luca Padovani, Polymorphic Endpoint Types for Copyless Message Passing, Proceedings of the 4^th Interaction and Concurrency Experience (ICE’11), pages 52-67, 2011.
  abstract bib slidespdf

  We present PolySing#, a calculus that models process interaction based on copyless message passing, in the style of Singularity OS. We equip the calculus with a type system that accommodates polymorphic endpoint types, which are a variant of polymorphic session types, and we show that well-typed processes are free from faults, leaks, and communication errors. The type system is essentially linear, although linearity alone may leave room for scenarios where well-typed processes leak memory. We identify a condition on endpoint types that prevents these leaks from occurring.

• Viviana Bono, Chiara Messa and Luca Padovani, Typing Copyless Message Passing, Proceedings of the 20^th European Symposium on Programming (ESOP’11), pages 57-76, 2011.
  abstract bib

  We present a calculus that models a form of process interaction based on copyless message passing, in the style of Singularity OS. The calculus is equipped with a type system ensuring that well-typed processes are free from faults, leaks, and communication errors. The type system is essentially linear, but we show that linearity alone is inadequate. On the one hand, it is too strict when dealing with heap-allocated objects; on the other hand, it leaves room for scenarios where well-typed processes leak significant amounts of memory. We address these problems using dedicated types for keeping track of dereferenced pointers and by basing the type system upon an original variant of session types.

2010

• Luca Padovani, Contract-Based Discovery of Web Services Modulo Simple Orchestrators, Theoretical Computer Science, pages 3328-3347, 2010.
  abstract bib

  Web services are distributed processes exposing a public description of their behavior, or contract. The availability of repositories of Web service descriptions enables interesting forms of dynamic Web service discovery, such as searching for Web services having a specified contract. This calls for a formal notion of contract equivalence satisfying two contrasting goals: being as coarse as possible so as to favor Web services reuse, and guaranteeing successful client/service interaction. We study an equivalence relation that achieves both goals under the assumption that client/service interactions may be mediated by simple orchestrators. In the framework we develop, orchestrators play the role of proofs (in the Curry-Howard sense) justifying an equivalence relation between contracts. This makes it possible to automatically synthesize orchestrators out of Web services contracts.

• Matteo Baldoni, Cristina Baroglio, Federico Bergenti, Antonio Boccalatte, Elisa Marengo, Maurizio Martelli, Viviana Mascardi, Luca Padovani, Viviana Patti, Alessandro Ricci, Gianfranco Rossi and Andrea Santi, MERCURIO: An Interaction-oriented Framework for Designing, Verifying and Programming Multi-Agent Systems, Proceedings of the 11^th International Workshop on Coordination, Organization, Institutions and Norms in Multi-Agent Systems (COIN’10), pages 134-149, 2010.
  abstract bib pdf

  This is a position paper reporting the motivations, the starting point and the guidelines that characterise the MERCURIO project proposal, submitted to MIUR PRIN 2009. The aim is to develop formal models of interactions and of the related support infrastructures, that overcome the limits of the current approaches by explicitly representing not only the agents but also the computational environment in terms of rules, conventions, resources, tools, and services that are functional to the coordination and cooperation of the agents. The models will enable the verification of interaction properties of MAS from the global point of view of the system as well as from the point of view of the single agents, due to the introduction a novel social semantic of interaction based on commitments and on an explicit account of the regulative rules.

2009

• Luca Padovani, Session Types at the Mirror, Proceedings of the 2^nd Interaction and Concurrency Experience (ICE’09), pages 71-86, 2009.
  abstract bib slidespdf

  We (re)define session types as projections of process behaviors with respect to the communication channels they use. In this setting, we give session types a semantics based on fair testing. The outcome is a unified theory of behavioral types that shares common aspects with conversation types and that encompass features of both dyadic and multi-party session types. The point of view we provide sheds light on the nature of session types and gives us a chance to reason about them in a framework where every notion, from well-typedness to the subtyping relation between session types, is semantically – rather than syntactically – grounded.

• Giuseppe Castagna, Mariangiola Dezani-Ciancaglini, Elena Giachino and Luca Padovani, Foundations of Session Types, Proceedings of the 11^th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP’09), pages 219-230, 2009.
  abstract bib ppdp Most Influential Paper

  We present a streamlined theory of session types based on a simple yet general and expressive formalism whose main eatures are semantically characterized and where each design choice is semantically justified. We formally define the semantics of session types and use it to devise the subsessioning relation. We give a coinductive characterization of subsessioning and describe algorithms to decide all the key relations defined in the article. We demonstrate the generality and expressive power of our framework by providing a session-based type system for a pi-calculus variant that does not rely on any specialized construct for session-based communication. The type system is shown to guarantee absence of communication errors and global progress.

• Samuele Carpineti, Cosimo Laneve and Luca Padovani, PiDuce - A Project for Experimenting Web Services Technologies, Science of Computer Programming, pages 777-811, 2009.
  abstract bib

  The PiDuce project comprises a programming language and a distributed runtime environment devised for experimenting Web services technologies by relying on solid theories about process calculi and formal languages for XML documents and schemas. The language features values and datatypes that extend XML documents and schemas with channels, an expressive type system with subtyping, a pattern matching mechanism for deconstructing XML values, and control constructs that are based on Milner’s asynchronous pi calculus. PiDuce programs are compiled into typesafe object code. The runtime environment supports the execution of PiDuce object code over networks by relying on state-of-the-art technologies, such as XML schema and WSDL, thus enabling interoperability with existing Web services. We thoroughly describe the PiDuce project: the programming language and its semantics, the architecture of the distributed runtime and its implementation. A running prototype is available at http://www.cs.unibo.it/PiDuce/.

• Giuseppe Castagna and Luca Padovani, Contracts for Mobile Processes, Proceedings of the 20^th International Conference on Concurrency Theory (CONCUR’09), pages 211-228, 2009.
  abstract bib slidespdf

  Theories identifying well-formed systems of processes – those that lack communication errors and enjoy strong properties such as deadlock freedom – are based either on session types, which are inhabited by channels, or on contracts, which are inhabited by processes. Current session type theories impose overly restrictive disciplines while contract theories only work for networks with fixed topology. Here we fill the gap between the two approaches by defining a theory of contracts for so-called mobile processes, those whose communications may include delegations and channel references.

• Giuseppe Castagna, Nils Gesbert and Luca Padovani, A Theory of Contracts for Web Services, ACM Transactions on Programming Languages and Systems, pages 19:1-19:61, 2009.
  abstract bib

  Contracts are behavioral descriptions of Web services. We devise a theory of contracts that formalizes the compatibility of a client to a service, and the safe replacement of a service with another service. The use of contracts statically ensures the successful completion of every possible interaction between compatible clients and services. The technical device that underlies the theory is the filter, which is an explicit coercion preventing some possible behaviors of services and, in doing so, make services compatible with different usage scenarios. We show that filters can be seen as proofs of a sound and complete subcontracting deduction system which simultaneously refines and extends Hennessy’s classical axiomatization of the must testing preorder. The relation is decidable and the decision algorithm is obtained via a cut-elimination process that proves the coherence of subcontracting as a logical system. Despite the richness of the technical development, the resulting approach is based on simple ideas and basic intuitions. Remarkably, its application is mostly independent of the language used to program the services or the clients. We outline the practical aspects of our theory by studying two different concrete syntaxes for contracts and applying each of them to Web services languages. We also explore implementation issues of filters and discuss the perspectives of future research this work opens.

• Luca Padovani, Contract-based Discovery and Adaptation of Web Services, International School on Formal Methods for the Design of Computer, Communication and Software Systems (SFM’09), pages 213-260, 2009.
  abstract slidespdf

  A contract describes the observable behavior of a Web service. When looking for Web services providing specific capabilities, the contract can be used as an important search key. This calls for a notion of contract equivalence that goes beyond nominal or structural equivalence. In this paper we define a simple, yet expressive formal language for describing Web service contracts. We provide a natural, set-theoretic semantics of contracts and we use it for defining a family of equivalence relations that can be effectively used for discovering and adapting Web services implementing a specific contract.

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

2008

• Luca Padovani, Contract-Directed Synthesis of Simple Orchestrators, Proceedings of the 19^th International Conference on Concurrency Theory (CONCUR’08), pages 131-146, 2008.
  abstract bib slidespdf

  The availability of repositories of Web service descriptions enables interesting forms of dynamic Web service discovery, such as searching for Web services exposing a specified behavior – or contract. This calls for a formal notion of contract equivalence satisfying two contrasting goals: being as coarse as possible so as to favor Web services reuse, and guaranteeing smooth client/service interaction. We study an equivalence relation under the assumption that interactions are controlled by orchestrators. We build a simple orchestration language on top of this theory and we show how to synthesize orchestrators out of Web services contracts.

• Cosimo Laneve and Luca Padovani, The Pairing of Contracts and Session Types, Concurrency, Graphs and Models (Ugo65’08), pages 681-700, 2008.
  abstract bib

  We pair session types and contracts using two encodings. The encoding of session types accommodates width and depth subtyping, two properties that partially hold in contracts. The encoding of contracts accommodates complex synchronization patterns, since session types own a simple control protocol. The encodings allow one to use the two formalisms interchangeably, within the context of dyadic interactions.

• Giuseppe Castagna, Nils Gesbert and Luca Padovani, A Theory of Contracts for Web Services, Proceedings of the 35^th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’08), pages 261-272, 2008.
  abstract bib

  Contracts are behavioural descriptions of Web services. We devise a theory of contracts that formalises the compatibility of a client to a service, and the safe replacement of a service with another service. The use of contracts statically ensures the successful completion of every possible interaction between compatible clients and services. The technical device that underlies the theory is the definition of filters, which are explicit coercions that prevent some possible behaviours of services and, in doing so, they make services compatible with different usage scenarios. We show that filters can be seen as proofs of a sound and complete subcontracting deduction system which simultaneously refines and extends Hennessy’s classical axiomatisation of the must testing preorder. The relation is decidable and the decision algorithm is obtained via a cut-elimination process that proves the coherence of subcontracting as a logical system. Despite the richness of the technical development, the resulting approach is based on simple ideas and basic intuitions. Remarkably, its application is mostly independent of the language used to program the services or the clients. We also outline the possible practical impact of such a work and the perspectives of future research it opens.

2007

• Cosimo Laneve and Luca Padovani, The Must Preorder Revisited - An Algebraic Theory for Web Services Contracts, Proceedings of the 18^th International Conference on Concurrency Theory (CONCUR’07), pages 212-225, 2007.
  abstract bib slidespdf

  We define a language for Web services contracts as a parallel-free fragment of ccs and we study a natural notion of compliance between clients and services in terms of their corresponding contracts. The induced contract preorder turns out to be valuable in searching and querying registries of Web services, it shows interesting connections with the must preorder, and it exhibits good precongruence properties when choreographies of Web services are considered. Our contract language may be used as a foundation of Web services technologies, such as wsdl and wscl.

• Marco Bernardo and Luca Padovani, Performance-Oriented Comparison of Web Services via Client-Specific Testing Preorders, Proceedings of the 9^th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS’07), pages 269-284, 2007.
  abstract bib

  The behavior of a Web service can be described by means of a contract, which is a specification of the legal interactions with the service. Given a repository of Web services, from the client viewpoint a proper service selection should be based on functional as well as non-functional aspects of the interactions. In this paper we provide a technique that enables a client both to discover compatible services and to compare them on the basis of specific performance requirements. Our technique, which is illustrated on a simple probabilistic calculus, relies on two families of client-specific probabilistic testing preorders. These are shown to be precongruences with respect to the operators of the language and not to collapse into equivalences unlike some more general probabilistic testing preorders appeared in the literature.

• Giuseppe Castagna, Nils Gesbert and Luca Padovani, A Theory of Contracts for Web Services, Proceedings of the ACM SIGPLAN Workshop on Programming Language Technologies for XML (PLAN-X’07), pages 37-48, 2007.
  abstract bib

  We report preliminary results on our attempt to devise a type theory to decribe the detailed behaviour of web services and relate them. Our goal is to devise a type system that is as much minimal and language neutral as possible. We outline the possible practical impact of such a work, and the perspectives of future research it opens.

2006

• Samuele Carpineti, Giuseppe Castagna, Cosimo Laneve and Luca Padovani, A Formal Account of Contracts for Web Services, Proceedings of the 3^rd International Workshop on Web Services and Formal Methods (WS-FM’06), pages 148-162, 2006.
  abstract bib slidespdf

  We define a formal contract language along with subcontract and compliance relations. We then extrapolate contracts out of processes, that are a recursion-free fragment of ccs. We finally demonstrate that a client completes its interactions with a service provided the corresponding contracts comply. Our contract language may be used as a foundation of Web services technologies, such as wsdl and wscl.

• Cosimo Laneve and Luca Padovani, Smooth Orchestrators, Proceedings of International Conference on Foundations of Software Science and Computation Structures (FoSSaCS’06), pages 32-46, 2006.
  abstract bib slidespdf

  A smooth orchestrator is a process with several alternative branches, every one defining synchronizations among co-located channels. Smooth orchestrators constitute a basic mechanism that may express standard workflow patterns in Web services as well as common synchronization constructs in programming languages. Smooth orchestrators may be created in one location and migrated to a different one, still not manifesting problems that usually afflict generic mobile agents. We encode an extension of Milner’s (asynchronous) pi calculus with join patterns into a calculus of smooth orchestrators and we yield a strong correctness result (full abstraction) when the subjects of the join patterns are co-located. We also study the translation of smooth orchestrators into finite-state automata, therefore addressing the implementation of co-location constraints and the case when synchronizations are not linear with respect to subjects.

• Luca Padovani and Stefano Zacchiroli, From Notation to Semantics: There and Back Again, Proceedings of the 5^th International Conference on Mathematical Knowledge Management (MKM’06), pages 194-207, 2006.
  abstract bib

  Mathematical notation is a structured, open, and ambiguous language. In order to support mathematical notation in MKM applications one must necessarily take into account presentational as well as semantic aspects. The former are required to create a familiar, comfortable, and usable interface to interact with. The latter are necessary in order to process the information meaningfully. In this paper we investigate a framework for dealing with mathematical notation in a meaningful, extensible way, and we show an effective instantiation of its architecture to the field of interactive theorem proving. The framework builds upon well-known concepts and widely-used technologies and it can be easily adopted by other MKM applications.

2005

• Nadia Busi and Luca Padovani, A Distributed Implementation of Mobile Nets as Mobile Agents, Proceedings of the 7^th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS’05), pages 259-274, 2005.
  abstract bib

  Mobile nets arise as a combination of the name managing techniques of the $\pi$-calculus with the representation of concurrency and locality of Petri nets. We propose MAGNETs, a variant of mobile nets that are suitable for an effective, distributed implementation. Such implementation extends an implementation of the Join calculus virtual machine with dynamic reconfiguration features.

• Luca Padovani, Compilation of Generic Regular Path Expressions Using C++ Class Templates, Proceedings of the 14^th International Conference on Compiler Construction (CC’05), pages 27-42, 2005.
  abstract bib slidespdf artifactgit

  Various techniques for the navigation and matching of data structures using path expressions have been the subject of extensive investigations. No matter whether such techniques are based on type information, indexing, automata, it is desirable to synthesize implementations automatically, starting from a high-level description of the path expressions to be traversed. In this paper we present a library of C++ templates for the representation of regular path expressions and their compilation into efficient backtracking algorithms. The resulting code can be used to implement visitors, pattern matchers, node collectors on regular paths over possibly heterogeneous, linked data structures. The point of the paper is on the path compilation technique, which was inspired by a continuation-passing, functional semantics of the path expressions. We rely on some peculiar aspects of C++ templates to create a compilation framework that closely follows the given semantics.

2004

• Luca Padovani, Claudio Sacerdoti Coen and Stefano Zacchiroli, A Generative Approach to the Implementation of Language Bindings for the Document Object Model, Proceedings of the 3^rd International Conference on Generative Programming and Component Engineering (GPCE’04), pages 469-487, 2004.
  abstract bib artifactweb

  The availability of a C implementation of the Document Object Model (DOM) offers the interesting opportunity of generating bindings for different programming languages automatically. Because of the DOM bias towards Java-like languages, a C implementation that fakes objects, inheritance, polymorphism, exceptions and uses reference-counting introduces a gap between the API specification and its actual implementation that the bindings should try to close. In this paper we overview the generative approach in this particular context and apply it for the generation of C++ and OCaml bindings.

• Luca Padovani and Riccardo Solmi, An Investigation on the Dynamics of Direct-Manipulation Editors for Mathematics, Proceedings of the 3^rd International Conference on Mathematical Knowledge Management (MKM’04), pages 302-316, 2004.
  abstract bib

  Mathematical expressions are pieces of structured information that could benefit from direct-manipulation approaches for document authoring. Yet, not only there is disagreement on the behaviors of authoring tools, but also these behaviors are often ill-designed and poorly implemented. This situation leads to dissatisfaction amid users who prefer more classical editing approaches. In this paper we compare the behaviors of several state-of-the-art editors for mathematical content and we try to synthesize a set of rules and principles to make the authoring experience pleasant and effective.

• Luca Padovani, A Math Canvas for the GNOME Desktop, Proceedings of the 5^th Annual GNOME User and Developer European Conference (GUADEC’04), 2004.
  abstract slidespdf

  In this paper we describe GtkMathView’s features for the creation of interactive, customizable applications involving rendering of mathematical markup. We also give an overview of the GtkMathView’s internal architecture and suggest some of the most promising future developments of the widget.

• Luca Padovani, Interactive Editing of MathML Markup Using TeX Syntax, Proceedings of the International Conference on TeX, XML, and Digital Typography (TUG’04), pages 125-138, 2004.
  abstract bib slidespdf

  We describe the architecture of a syntax-directed editor for authoring structured mathematical documents that can be used for the generation of MathML markup. The author interacts with the editor by typing TeX markup as in a normal text editor, with the difference that the typed markup is parsed and displayed on-the-fly. We discuss issues regarding both the parsing and presentation phases and we propose implementations for them. In contrast with existing similar tools, the architecture we propose offers better compatibility with TeX syntax, a pervasive use of standard technologies and a clearer separation of content and presentation aspects of the information.

2003

• Luca Padovani, On the Roles of LaTeX and MathML in Encoding and Processing Mathematical Expressions, Proceedings of the 2^nd International Conference on Mathematical Knowledge Management (MKM’03), pages 66-79, 2003.
  abstract bib

  The Mathematical Markup Language (MathML), a standard language for the encoding of mathematical expressions, is going to have a deep impact on a vast community of users, from people interested in publishing scientific documents to researchers who seek new forms of communication and management of mathematical information. In this paper we survey the worlds of LaTeX, a well-established language for typesetting, and MathML, whose diffusion is promisingly taking off in these days, with an emphasis on the management of mathematics. We will try to understand how they relate to each other, and why we will still need both in the years to come.

• Luca Padovani, MathML Formatting with TeX Rules, TeX Fonts, and TeX Quality, The Communications of the TeX Users Group, pages 53-61, 2003.
  abstract pdf artifactweb

  In this paper we investigate the architecture of a MathML formatting engine based on an abstraction of the TeX box primitives. This engine is carefully designed so that the TeX-dependent formatting rules are isolated from the independent ones and is capable of achieving TeX-comparable output quality when used in conjunction with TeX fonts. We show how the formatting rules presented in Appendix G of the TeXbook can be easily adapted for MathML formatting, and how the semantically-rich MathML markup simplifies the rules themselves.

• Andrea Asperti, Luca Padovani, Claudio Sacerdoti Coen, Ferruccio Guidi and Irene Schena, Mathematical Knowledge Management in HELM, Annals of Mathematics and Artificial Intelligence, pages 27-46, 2003.
  abstract bib

  The paper describes the general philosophy and the main architectural and technological solutions adopted in the HELM Project for the management of large repositories of mathematical knowledge. The leitmotiv is the extensive use of XML technology, and the exploitation of information in the "Web way", that is without a central authority, with few basic rules, in a scalable, adaptable, and extensible manner.

2002

• Paolo Casarini and Luca Padovani, The GNOME DOM Engine, Markup Languages: Theory & Practice, pages 173-190, 2002.
  abstract artifactweb

  The widespread use of Web technologies and, in particular, the ever growing number of applications adopting XML as the standard language for the encoding of any piece of structured information, naturally calls for efficient implementations of DOM, the standard interface to access the internal structure of documents. The DOM level 2 API, which has been conceived as a suitable hierarchy of classes, has its most natural mapping in object-oriented languages such as C++ and Java. This is also testified by the already existing implementations in those languages. However, as of today, most applications are commonly developed in C, because of its standardization, flexibility, efficiency and availability. In this paper we describe the current state of Gdome2, which provides a DOM implementation for the C programming language. The library is meant to become a key module of the Gnome architecture, supplying a range of facilities for an efficient, portable, and easy management of XML documents in the Gnome way. We conclude with a comparison between Gdome2 and Xerces, one of the more advanced and actively developed DOM implementations.

• Luca Padovani, A Standalone Rendering Engine for MathML, Proceedings of the MathML International Conference (MathML’02), pages 109-114, 2002.
  artifactweb
• Yuzhen Xie, Stephen M. Watt and Luca Padovani, A Lisp Subset Based on MathML, Proceedings of the MathML International Conference (MathML’02), pages 101-108, 2002.
  pdf

2001

• Andrea Asperti, Luca Padovani, Claudio Sacerdoti Coen and Irene Schena, HELM and the Semantic Math-Web, Proceedings of the International Conference on Theorem Proving in Higher Order Logics (TPHOLs’01), pages 59-74, 2001.
  abstract bib

  The eXtensible Markup Language (XML) opens the possibility to start anew, on a solid technological ground, the ambitious goal of developing a suitable technology for the creation and maintenance of a virtual, distributed, hypertextual library of formal mathematical knowledge. In particular, XML provides a central technology for storing, retrieving and processing mathematical documents, comprising sophisticated web-publishing mechanisms (stylesheets) covering notational and stylistic issues. By the application of XML technology to the large repositories of structured, content oriented information offered by Logical Frameworks we meet the ultimate goal of the Semantic Web, that is to allow machines the sharing and exploitation of knowledge in the Web way, i.e. without central authority, with few basic rules, in a scalable, adaptable, extensible manner.

• Andrea Asperti, Luca Padovani, Claudio Sacerdoti Coen and Irene Schena, XML, Stylesheets and the Re-mathematization of Formal Content, Proceedings of the Extreme Markup Languages Conference (EXTREME’01), pages 17-27, 2001.
  abstract bib pdf

  An important part of the descriptive power of mathematics derives from its ability to represent formal concepts in a highly evolved, two-dimensional system of symbolic notations. Tools for the mechanisation of mathematics and the automation of formal reasoning must eventually face the problem of re-mathematization of the logical, symbolic content of the information, especially in view of their integration with the World Wide Web. In a different work we already discussed the pivotal role that XML (eXtensible Markup Language) technology is likely to play in such an integration. In this paper, we focus on the problem of (Web) publishing, advocating the use of XSL (eXtensible Stylesheet Language) Transformations, in conjunction with MathML (Mathematical Markup Language), as a standard, application independent and modular way for associating notation to formal mathematical content.

• Paolo Casarini and Luca Padovani, The GNOME DOM Engine, Proceedings of the Extreme Markup Languages Conference (EXTREME’01), pages 45-53, 2001.
  abstract bib pdf artifactweb

  The widespread use of Web technologies and, in particular, the ever growing number of applications adopting XML as the standard language for the encoding of any piece of structured information, naturally calls for efficient implementations of DOM, the standard interface to access the internal structure of documents. The DOM level 2 API, which has been conceived as a suitable hierarchy of classes, has its most natural mapping in object-oriented languages such as C++ and Java. This is also testified by the already existing implementations in those languages. However, as of today, most applications are commonly developed in C, because of its standardization, flexibility, efficiency and availability. In this paper we describe the current state of Gdome2, which provides a DOM implementation for the C programming language. The library is meant to become a key module of the Gnome architecture, supplying a range of facilities for an efficient, portable, and easy management of XML documents in the Gnome way. We conclude with a comparison between Gdome2 and Xerces, one of the more advanced and actively developed DOM implementations.

• Andrea Asperti, Luca Padovani, Claudio Sacerdoti Coen and Irene Schena, Formal Mathematics on the Web, Proceedings of the 8^th International Conference on Libraries and Associations in the Transient World: New Technologies and New Forms of Cooperation (Crimea’01), pages 342-346, 2001.
  web

News

A solution of the linearity challenge

15 October 2024

Claudia Raffaelli and I have been working on an Agda solution of the linearity challenge that was proposed earlier this year in the Concurrent Calculi Formalisation Benchmark. Our solution formalizes πLIN – a linear π-calculus based on linear logic – using the context splitting technique. This technique is traditionally considered heavy but we find that in the setting of πLIN it works very well. The formalisation is publicly available on GitHub, with further developments coming soon.

Back to Bologna!

01 October 2024

I have joined the Department of Computer Science and Engineering of the University of Bologna. It’s both humbling and exciting to be working together with all the great people who taught me computer science.

Astrophotography

I like to take photos of (deep-)sky objects. Below are some of my best photos in reverse chronological order. Hover to magnify and right-click to download. These images are licensed under a Creative Commons Attribution-ShareAlike 4.0 License.