15 citations · 40 across the 14 of their papers we have counts for
17 papers
A monadic interpreter and type-and-effect checker
Stefano Raviola, Paola Giannini, Francesco Dagnino
We present a concrete implementation in Haskell of a monadic framework that includes both a small-step interpreter and a type-and-effect checker for the corresponding language. Our…
Free constructions for comprehension categories
Francesco Dagnino, Jacopo Emmenegger, Andrea Giusto
Jacobs comprehension categories subsume a large class of categorical models of type dependency, supporting also the description of morphisms between types. We study the relationshi…
Fair Termination for Resource-Aware Active Objects
Francesco Dagnino, Paola Giannini, Violet Ka I Pun +1
Active object systems are a model of distributed computation that has been adopted for modelling distributed systems and business process workflows. This field of modelling is, in…
Don't exhaust, don't waste: Resource-aware soundness for big-step semantics
Riccardo Bianchini, Francesco Dagnino, Paola Giannini +1
We extend the semantics and type system of a lambda calculus equipped with common constructs to be "resource-aware". That is, the semantics keeps track of the usage of resources, a…
An effectful object calculus
Francesco Dagnino, Paola Giannini, Elena Zucca
We show how to smoothly incorporate in the object-oriented paradigm constructs to raise, compose, and handle effects in an arbitrary monad. The underlying pure calculus is meant to…
Monadic type-and-effect soundness
Francesco Dagnino, Paola Giannini, Elena Zucca
We introduce the abstract notions of "monadic operational semantics", a small-step semantics where computational effects are modularly modeled by a monad, and "type-and-effect syst…
Multi-graded Featherweight Java
Riccardo Bianchini, Francesco Dagnino, Paola Giannini +1
Resource-aware type systems statically approximate not only the expected result type of a program, but also the way external resources are used, e.g., how many times the value of a…
Coeffects for Sharing and Mutation
Riccardo Bianchini, Francesco Dagnino, Paola Giannini +2
In type-and-coeffect systems, contexts are enriched by coeffects modeling how they are actually used, typically through annotations on single variables. Coeffects are computed bott…
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 ca…
A meta-theory for big-step semantics
Francesco Dagnino
It is well-known that big-step semantics is not able to distinguish stuck and non-terminating computations. This is a strong limitation as it makes very difficult to reason about p…
Flexible coinductive logic programming
Francesco Dagnino, Davide Ancona, Elena Zucca
Recursive definitions of predicates are usually interpreted either inductively or coinductively. Recently, a more powerful approach has been proposed, called flexible coinduction,…
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 tha…
Sound Regular Corecursion in coFJ
Davide Ancona, Pietro Barbieri, Francesco Dagnino +1
The aim of the paper is to provide solid foundations for a programming paradigm natively supporting the creation and manipulation of cyclic data structures. To this end, we describ…
Soundness conditions for big-step semantics
Francesco Dagnino, Viviana Bono, Elena Zucca +1
We propose a general proof technique to show that a predicate is sound, that is, prevents stuck computation, with respect to a big-step semantics. This result may look surprising,…
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,…
Generalizing inference systems by coaxioms
Francesco Dagnino
After surveying classical results, we introduce a generalized notion of inference system to support structural recursion on non-well-founded data types. Besides axioms and inferenc…
Extending Coinductive Logic Programming with Co-Facts
Davide Ancona, Francesco Dagnino, Elena Zucca
We introduce a generalized logic programming paradigm where programs, consisting of facts and rules with the usual syntax, can be enriched by co-facts, which syntactically resemble…