11 citations · 27 across the 11 of their papers we have counts for
13 papers
Operational methods in semantics
Roberto M. Amadio
The focus of these lecture notes is on abstract models and basic ideas and results that relate to the operational semantics of programming languages largely conceived. The approach…
Certifying and reasoning about cost annotations of functional programs
Roberto M. Amadio, Yann Regis-Gianas
We present a so-called labelling method to insert cost annotations in a higher-order functional program, to certify their correctness with respect to a standard compilation chain t…
A decompilation of the pi-calculus and its application to termination
Roberto Amadio
We study the correspondence between a concurrent lambda-calculus in administrative, continuation passing style and a pi-calculus and we derive a termination result for the latter.
Elementary affine -calculus with multithreading and side effects
Antoine Madet, Roberto M. Amadio
Linear logic provides a framework to control the complexity of higher-order functional programs. We present an extension of this framework to programs with multithreading and side…
Certifying cost annotations in compilers
Roberto M. Amadio, Nicolas Ayache, Yann Régis-Gianas +1
We discuss the problem of building a compiler which can lift in a provably correct way pieces of information on the execution cost of the object code to cost annotations on the sou…
An affine-intuitionistic system of types and effects: confluence and termination
Roberto Amadio, Patrick Baillot, Antoine Madet
We present an affine-intuitionistic system of types and effects which can be regarded as an extension of Barber-Plotkin Dual Intuitionistic Linear Logic to multi-threaded programs…