20 citations · 96 across the 24 of their papers we have counts for
25 papers
An Infinitary Lambda Calculus with Global Trace Condition (Extended Abstract)
Stefano Berardi, Ugo de' Liguoro, Daisuke Kimura +1
We consider an extension of the infinitary lambda calculus by Kennaway et al., with zero, successor, and conditional, and a type system akin to Goedel's system T. For terms that ca…
Logics and Type Theory: essays dedicated to Stefano Berardi on the occasion of his 1000000th birthday
Thorsten Altenkirch, Franco Barbanera, Ferruccio Damiani +1
Proof Theory and Type Theory are two branches of mathematical logic and theoretical computer science that explore the structure of mathematical proofs and the foundations of comput…
Partial Typing for Asynchronous Multiparty Sessions
Franco Barbanera, Mariangiola Dezani-Ciancaglini, Ugo de'Liguoro
Formal verification methods for concurrent systems cannot always be scaled-down or tailored in order to be applied on specific subsystems. We address such an issue in a MultiParty…
From Semantics to Types: the Case of the Imperative lambda-Calculus
Ugo de'Liguoro, Riccardo Treglia
We propose an intersection type system for an imperative lambda-calculus based on a state monad and equipped with algebraic operations to read and write to the store. The system is…
Intersection Types for a Computational Lambda-Calculus with Global State
Ugo de'Liguoro, Riccardo Treglia
We study the semantics of an untyped lambda-calculus equipped with operators representing read and write operations from and to a global store. We adopt the monadic approach to mod…
Towards Refinable Choreographies
Ugo de'Liguoro, Hernán Melgratti, Emilio Tuosto
We investigate refinement in the context of choreographies. We introduce refinable global choreographies allowing for the underspecification of protocols, whose interactions can be…
Intersection Types for the Computational lambda-Calculus
Ugo de'Liguoro, Riccardo Treglia
We study polymorphic type assignment systems for untyped lambda-calculi with effects, based on Moggi's monadic approach. Moving from the abstract definition of monads, we introduce…
Global Types for Open Systems
Franco Barbanera, Ugo de'Liguoro, Rolf Hennicker
Global-type formalisms enable to describe the overall behaviour of distributed systems and at the same time to enforce safety properties for communications between system component…
Mailbox Types for Unordered Interactions
Ugo de'Liguoro, Luca Padovani
We propose a type system for reasoning on protocol conformance and deadlock freedom in networks of processes that communicate through unordered mailboxes. We model these networks i…
Mixin Composition Synthesis based on Intersection Types
Jan Bessai, Tzu-Chun Chen, Andrej Dudenhefner +3
We present a method for synthesizing compositions of mixins using type inhabitation in intersection types. First, recursively defined classes and mixins, which are functions over c…
Session Types for Orchestrated Interactions
Franco Barbanera, Ugo de'Liguoro
In the setting of the pi-calculus with binary sessions, we aim at relaxing the notion of duality of session types by the concept of retractable compliance developed in contract the…
Intersection Types for the lambda-mu Calculus
Steffen van Bakel, Franco Barbanera, Ugo de'Liguoro
We introduce an intersection type system for the lambda-mu calculus that is invariant under subject reduction and expansion. The system is obtained by describing Streicher and Reus…
Retractability, games and orchestrators for session contracts
Franco Barbanera, Ugo de'Liguoro
Session contracts is a formalism enabling to investigate client/server interaction protocols and to interpret session types. We extend session contracts in order to represent outpu…
Secure Multiparty Sessions with Topics
Ilaria Castellani, Mariangiola Dezani-Ciancaglini, Ugo de'Liguoro
Multiparty session calculi have been recently equipped with security requirements, in order to guarantee properties such as access control and leak freedom. However, the proposed s…
Proceedings of the Workshop on Continuations
Olivier Danvy, Ugo de'Liguoro
The notion of continuation is ubiquitous in many different areas of computer science, including systems programming, programming languages, algorithmics, semantics, logic, and cons…
Retractable Contracts
Franco Barbanera, Mariangiola Dezani-Ciancaglini, Ivan Lanese +1
In calculi for modelling communication protocols, internal and external choices play dual roles. Two external choices can be viewed naturally as dual too, as they represent an agre…
Orchestrated Session Compliance
Franco Barbanera, Steffen van Bakel, Ugo de'Liguoro
We investigate the notion of orchestrated compliance for client/server interactions in the context of session contracts. Devising the notion of orchestrator in such a context makes…
Typing Classes and Mixins with Intersection Types
Jan Bessai, Boris Düdder, Andrej Dudenhefner +2
We study an assignment system of intersection types for a lambda-calculus with records and a record-merge operator, where types are preserved both under subject reduction and expan…
Compliance for reversible client/server interactions
Franco Barbanera, Mariangiola Dezani-Ciancaglini, Ugo de' Liguoro
In the setting of session behaviours, we study an extension of the concept of compliance when a disciplined form of backtracking is present. After adding checkpoints to the syntax…
Knowledge Spaces and the Completeness of Learning Strategies
Stefano Berardi, Ugo de'Liguoro
We propose a theory of learning aimed to formalize some ideas underlying Coquand's game semantics and Krivine's realizability of classical logic. We introduce a notion of knowledge…
Proceedings First Workshop on Control Operators and their Semantics
Ugo de'Liguoro, Alexis Saurin
The focus of the papers presented in this volume is on the interplay between syntax and semantics in case of languages, namely the central question of what a program means and how…
Non-monotonic Pre-fixed Points and Learning
Stefano Berardi, Ugo de' Liguoro
We consider the problem of finding pre-fixed points of interactive realizers over arbitrary knowledge spaces, obtaining a relative recursive procedure. Knowledge spaces and interac…
Characterisation of Strongly Normalising lambda-mu-Terms
Steffen van Bakel, Franco Barbanera, Ugo de'Liguoro
We provide a characterisation of strongly normalising terms of the lambda-mu-calculus by means of a type system that uses intersection and product types. The presence of the latter…
Proceedings Fourth Workshop on Classical Logic and Computation
Herman Geuvers, Ugo de'Liguoro
CL&C'12 was the fourth of a conference series on "Classical Logic and Computation", held as satellite to ICALP'12 on Sunday July 8, 2012 in Warwick, England. CL&C intends to cover…