Search

• < Previous
• 1
• Next >

---

Coaxioms: flexible coinductive definitions by inference systems

Francesco Dagnino.

We introduce a generalized notion of inference system to support more flexible interpretations of recursive definitions. Besides axioms and inference rules with the usual meaning, we allow also coaxioms, which are, intuitively, axioms which can only be applied "at infinite depth" in a proof tree.&nbsp;[&hellip;]

---

A Fibrational Tale of Operational Logical Relations: Pure, Effectful and Differential

Francesco Dagnino ; Francesco Gavazzo.

Logical relations built on top of an operational semantics are one of the most successful proof methods in programming language semantics. In recent years, more and more expressive notions of operationally-based logical relations have been designed and applied to specific families of languages.&nbsp;[&hellip;]

---

Foundations of regular coinduction

Francesco Dagnino.

Inference systems are a widespread framework used to define possibly recursive predicates by means of inference rules. They allow both inductive and coinductive interpretations that are fairly well-studied. In this paper, we consider a middle way interpretation, called regular, which combines&nbsp;[&hellip;]

---

Deconfined Global Types for Asynchronous Sessions

Francesco Dagnino ; Paola Giannini ; Mariangiola Dezani-Ciancaglini.

Multiparty sessions with asynchronous communications and global types play an important role for the modelling of interaction protocols in distributed systems. In designing such calculi the aim is to enforce, by typing, good properties for all participants, maximising, at the same time, the accepted&nbsp;[&hellip;]

---