ABOUT ME
I am professor of Computer Science at the Department of Computer Science and Engineering of the University of Bologna. My research interests include programming languages, type systems, concurrency theory and formal software verification. On clear nights, I'm also an amateur astrophotographer.
CONTACT ME
PROFILES
- Pagina istituzionale (english)
- DBLP computer science bibliography
- Scopus
- ORCiD
- Google Scholar
- GitHub
- Social networks? No thanks.
Publications
2024
- Ugo Dal Lago and Luca Padovani, On the Almost-Sure Termination of Binary Sessions, Proceedings of the 26th International Symposium on Principles and Practice of Declarative Programming (PPDP’24), 2024.
- Francesco Dagnino and Luca Padovani, sMALL CaPS: An Infinitary Linear Logic for a Calculus of Pure Sessions, Proceedings of the 26th International Symposium on Principles and Practice of Declarative Programming (PPDP’24), 2024.
- 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 26th International Symposium on Formal Methods (FM’24), 2024.
- Ross Horne and Luca Padovani, A Logical Account of Subtyping for Session Types, Journal of Logical and Algebraic Methods in Programming, 2024.
-
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 26th International Conference on Coordination Models and Languages (COORDINATION’24),
pages 149-158,
2024.
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.
2023
- Ilaria Castellani, Ornela Dardha, Luca Padovani and Davide Sangiorgi, EXPRESSing Session Types, Proceedings of the Combined 30th International Workshop on Expressiveness in Concurrency and 20th Workshop on Structural Operational Semantics (EXPRESS/SOS’23), pages 8-25, 2023.
- Ross Horne and Luca Padovani, A Logical Account of Subtyping for Session Types, Proceedings of the 14th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES’23), pages 26-37, 2023.
2022
- Luca Padovani, On the Fair Termination of Client-Server Sessions, Proceedings of the 28th International Conference on Types for Proofs and Programs (TYPES’22), pages 5:1-5:21, 2022.
- Luca Ciccone and Luca Padovani, An Infinitary Proof Theory of Linear Logic Ensuring Fair Termination in the Linear π-Calculus, Proceedings of the 33rd International Conference on Concurrency Theory (CONCUR’22), pages 36:1-36:18, 2022.
- 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.
- Luca Ciccone, Francesco Dagnino and Luca Padovani, Fair Termination of Multiparty Sessions, Proceedings of the 36th European Conference on Object-Oriented Programming (ECOOP’22), pages 26:1-26:26, 2022.
-
Stephanie Balzer and
Luca Padovani,
Preface to the special issue on the 12th workshop on programming language approaches to concurrency and communication-centric software (PLACES) 2020,
Journal of Logical and Algebraic Methods in Programming,
2022.
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.
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.
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 48th International Colloquium on Automata, Languages, and Programming (ICALP’21), pages 125:1-125:16, 2021.
2020
- Luca Ciccone and Luca Padovani, A Dependently Typed Linear π-Calculus in Agda, Proceedings of the 22nd International Symposium on Principles and Practice of Declarative Programming (PPDP’20), pages 8:1-8:14, 2020.
- Omar Inverso, Hernán Melgratti, Luca Padovani, Catia Trubiani and Emilio Tuosto, Probabilistic Analysis of Binary Sessions, Proceedings of the 31st International Conference on Concurrency Theory (CONCUR’20), pages 14:1-14:21, 2020.
- Stephanie Balzer and Luca Padovani, Proceedings of the 12th International Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software, 2020.
2019
- Rosita Gerbo and Luca Padovani, Concurrent Typestate-Oriented Programming in Java, Proceedings of the 11th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES’19), pages 24-34, 2019.
- Giuseppe Castagna, Mariangiola Dezani-Ciancaglini, Elena Giachino and Luca Padovani, Foundations of Session Types: 10 Years Later, Proceedings of the 21st International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP’19), pages 1:1-1:3, 2019.
- Luca Padovani, Context-Free Session Type Inference, ACM Transactions on Programming Languages and Systems, pages 9:1-9:37, 2019.
- 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.
2018
- Ugo Liguoro and Luca Padovani, Mailbox Types for Unordered Interactions, Proceedings of the 32nd European Conference on Object-Oriented Programming (ECOOP’18), pages 15:1-15:28, 2018.
- Luca Padovani, A Type Checking Algorithm for Concurrent Object Protocols, Journal of Logical and Algebraic Methods in Programming, pages 16-35, 2018.
- Luca Padovani, Deadlock-Free Typestate-Oriented Programming, Programming Journal, pages article 15, 2018.
-
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.
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.
- 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.
- Paula Severi, Luca Padovani, Emilio Tuosto and Mariangiola Dezani-Ciancaglini, On Sessions and Infinite Data, Logical Methods in Computer Science, pages 1-39, 2017.
- Luca Padovani, A Simple Library Implementation of Binary Sessions, Journal of Functional Programming, 2017.
- Luca Padovani, Context-Free Session Type Inference, Proceedings of the 26th European Symposium on Programming (ESOP’17), pages 804-830, 2017.
- Hernán Melgratti and Luca Padovani, An OCaml Implementation of Binary Sessions, Behavioural Types: from Theory to Tools, pages 243-263, 2017.
- Luca Padovani, Type-Based Analysis of Linear Communications, Behavioural Types: from Theory to Tools, pages 193-217, 2017.
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.
- 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.
-
Paula Severi,
Luca Padovani,
Emilio Tuosto and
Mariangiola Dezani-Ciancaglini,
On Sessions and Infinite Data,
Proceedings of the 18th 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.
- 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.
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.
- Luca Padovani, Type Reconstruction for the Linear π-Calculus with Composite Regular Types, Logical Methods in Computer Science, pages 1-45, 2015.
- 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.
- Luca Padovani, Tzu-Chun Chen and Andrea Tosatto, Type Reconstruction Algorithms for Deadlock-Free and Lock-Free Linear π-Calculi, Proceedings of the 17th International Conference on Coordination Models and Languages (COORDINATION’15), pages 83-98, 2015.
- Cosimo Laneve and Luca Padovani, An Algebraic Theory for Web Service Contracts, Formal Aspects of Computing, pages 613-640, 2015.
- 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.
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.
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 16th International Conference on Coordination Models and Languages (COORDINATION’14),
pages 147-162,
2014.
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.
- Luca Padovani, Type Reconstruction for the Linear π-Calculus with Composite and Equi-Recursive Types, Proceedings of the 17th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS’14), pages 88-102, 2014.
-
Svetlana Jakšić and
Luca Padovani,
Exception Handling for Copyless Messaging,
Science of Computer Programming,
pages 22-51,
2014.
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 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’14), pages 5-17, 2014.
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.
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 40th International Colloquium on Automata, Languages and Programming (ICALP’13), Part II, pages 373-384, 2013.
- Mario Coppo, Mariangiola Dezani-Ciancaglini, Luca Padovani and Nobuko Yoshida, Inference of Global Progress Properties for Dynamically Interleaved Multiparty Sessions, Proceedings of the 15th International Conference on Coordination Models and Languages (COORDINATION’13), pages 45-59, 2013.
-
Mario Coppo,
Mariangiola Dezani-Ciancaglini,
Luca Padovani and
Nobuko Yoshida,
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.
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.
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 10th International Conference on Integrated Formal Methods (IFM’13),
pages 301-315,
2013.
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.
-
Luca Padovani,
On Projecting Processes into Session Types,
Mathematical Structures in Computer Science,
pages 237-289,
2012.
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 11th International Conference on Generative Programming and Component Engineering (GPCE’12),
pages 1-10,
2012.
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 14th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP’12),
pages 151-162,
2012.
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.
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.
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.
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 13th International Conference on Coordination Models and Languages (COORDINATION’11),
pages 127-141,
2011.
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 4th Interaction and Concurrency Experience (ICE’11),
pages 52-67,
2011.
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 20th European Symposium on Programming (ESOP’11),
pages 57-76,
2011.
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.
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 11th International Workshop on Coordination, Organization, Institutions and Norms in Multi-Agent Systems (COIN’10),
pages 134-149,
2010.
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 2nd Interaction and Concurrency Experience (ICE’09),
pages 71-86,
2009.
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 11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP’09),
pages 219-230,
2009.
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.
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 20th International Conference on Concurrency Theory (CONCUR’09),
pages 211-228,
2009.
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.
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.
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.
2008
-
Luca Padovani,
Contract-Directed Synthesis of Simple Orchestrators,
Proceedings of the 19th International Conference on Concurrency Theory (CONCUR’08),
pages 131-146,
2008.
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.
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 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’08),
pages 261-272,
2008.
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 18th International Conference on Concurrency Theory (CONCUR’07),
pages 212-225,
2007.
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 9th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS’07),
pages 269-284,
2007.
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.
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 3rd International Workshop on Web Services and Formal Methods (WS-FM’06),
pages 148-162,
2006.
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.
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 5th International Conference on Mathematical Knowledge Management (MKM’06),
pages 194-207,
2006.
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 7th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS’05),
pages 259-274,
2005.
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 14th International Conference on Compiler Construction (CC’05),
pages 27-42,
2005.
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 3rd International Conference on Generative Programming and Component Engineering (GPCE’04),
pages 469-487,
2004.
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 3rd International Conference on Mathematical Knowledge Management (MKM’04),
pages 302-316,
2004.
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 5th Annual GNOME User and Developer European Conference (GUADEC’04),
2004.
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.
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 2nd International Conference on Mathematical Knowledge Management (MKM’03),
pages 66-79,
2003.
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.
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.
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.
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.
- 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.
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.
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.
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.
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 8th International Conference on Libraries and Associations in the Transient World: New Technologies and New Forms of Cooperation (Crimea’01), pages 342-346, 2001.
News
The Great Orion Nebula
16 November 2024
This is what the Great Orion Nebula looks like under a nearly full moon, approximately 50˚ away. Total esposure time: 4 hours. More astrophotography below.
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.
Erlang workshop and ICTCS
11 March 2024
I’m excited to be a program committee member of Erlang 2024, the 23rd ACM SIGPLAN Erlang Workshop that will be organized as a co-located event affiliated with ICFP 2024, and of ICTCS 2024, the 25th Italian Conference on Theoretical Computer Science. This year ICFP will be held in Milan and ICTCS in Turin!
Astrophotography
I like to take pictures of distant objects. Below are some of my best pictures in reverse chronological order. High resolution pictures available on request.
06 September 2024
02 August 2024
11 July 2024
06 July 2024
07 June 2024
01 June 2024
12 May 2024
07 April 2024
28 March 2024
13 March 2024
12 March 2024
12 March 2024
25 February 2024
20 February 2024
14 February 2024
13 February 2024
03 February 2024
27 September 2023
12 September 2023
21 August 2023
16 August 2023
Quotes
“In the modern world the stupid are cocksure while the intelligent are full of doubt”, Bertrand Russell, 1933