6 citations · 9 across the 6 of their papers we have counts for
6 papers
Proceedings of the 18th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice
Alberto Ciaffaglione, Carlos Olarte
Logical frameworks and meta-languages form a common substrate for representing, implementing and reasoning about a wide variety of deductive systems of interest in logic and comput…
A Definitional Implementation of the Lax Logical Framework LLFP in Coq, for Supporting Fast and Loose Reasoning
Fabio Alessi, Alberto Ciaffaglione, Pietro Di Gianantonio +2
The Lax Logical Framework, LLFP, was introduced, by a team including the last two authors, to provide a conceptual framework for integrating different proof development tools, thus…
A prototype-based approach to object reclassification
Ciaffaglione Alberto, Di Gianantonio Pietro, Honsell Furio +1
We investigate, in the context of functional prototype-based lan- guages, a calculus of objects which might extend themselves upon receiving a message, a capability referred to by…
Lambda-calculus and Reversible Automatic Combinators
Alberto Ciaffaglione, Furio Honsell, Marina Lenisa +1
In 2005, Abramsky introduced various linear/affine combinatory algebras of partial involutions over a suitable formal language, to discuss reversible computation in a game-theoreti…
A weak HOAS approach to the POPLmark Challenge
Alberto Ciaffaglione, Ivan Scagnetto
Capitalizing on previous encodings and formal developments about nominal calculi and type systems, we propose a weak Higher-Order Abstract Syntax formalization of the type language…
A coinductive semantics of the Unlimited Register Machine
Alberto Ciaffaglione
We exploit (co)inductive specifications and proofs to approach the evaluation of low-level programs for the Unlimited Register Machine (URM) within the Coq system, a proof assistan…