15 citations · 40 across the 14 of their papers we have counts for
12 papers · 1 filter
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…
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…
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,…
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,…
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…