Alberto Ciaffaglione

23 papers B 3C 1Journal 8Unranked 9
YearRankTypeTitle / Venue / Authors
2023 — ed.
Proceedings of the 18th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FSCD 2023, Rome, Italy, 2nd July 2023.
LFMTP@FSCD
Alberto Ciaffaglione, Carlos Olarte
2021 J jnl
A protoype-based approach to object evolution.
J. Object Technol.
Alberto Ciaffaglione, Pietro Di Gianantonio, Furio Honsell, Luigi Liquori
2019 — conf
A Definitional Implementation of the Lax Logical Framework LLFP in Coq, for Supporting Fast and Loose Reasoning.
LFMTP@LICS
Fabio Alessi, Alberto Ciaffaglione, Pietro Di Gianantonio, Furio Honsell, Marina Lenisa
2019 J jnl
LF+ in Coq for "fast and loose" reasoning.
J. Formaliz. Reason.
Fabio Alessi, Alberto Ciaffaglione, Pietro Di Gianantonio, Furio Honsell, Marina Lenisa, Ivan Scagnetto
2019 B conf
lambda!-calculus, Intersection Types, and Involutions.
FSCD
Alberto Ciaffaglione, Pietro Di Gianantonio, Furio Honsell, Marina Lenisa, Ivan Scagnetto
2018 J jnl
A prototype-based approach to object reclassification.
CoRR
Alberto Ciaffaglione, Pietro Di Gianantonio, Furio Honsell, Luigi Liquori
2018 J jnl
Linear lambda-calculus and Reversible Automatic Combinators.
CoRR
Alberto Ciaffaglione, Furio Honsell, Marina Lenisa, Ivan Scagnetto
2018 B conf
The involutions-as-principal types/application-as-unification Analogy.
LPAR
Alberto Ciaffaglione, Furio Honsell, Marina Lenisa, Ivan Scagnetto
2016 J jnl
Towards Turing computability via coinduction.
Sci. Comput. Program.
Alberto Ciaffaglione
2015 J jnl
Mechanizing type environments in weak HOAS.
Theor. Comput. Sci.
Alberto Ciaffaglione, Ivan Scagnetto
2014 — conf
A Coinductive Animation of Turing Machines.
SBMF
Alberto Ciaffaglione
2014 — conf
Internal Adequacy of Bookkeeping in Coq.
LFMTP
Alberto Ciaffaglione, Ivan Scagnetto
2012 — conf
A weak HOAS approach to the POPLmark Challenge
LSFA
Alberto Ciaffaglione, Ivan Scagnetto
2011 — conf
A coinductive semantics of the Unlimited Register Machine
INFINITY
Alberto Ciaffaglione
2007 J jnl
Reasoning about Object-based Calculi in (Co)Inductive Type Theory and the Theory of Contexts.
J. Autom. Reason.
Alberto Ciaffaglione, Luigi Liquori, Marino Miculan
2006 J jnl
A certified, corecursive implementation of exact real numbers.
Theor. Comput. Sci.
Alberto Ciaffaglione, Pietro Di Gianantonio
2005 C conf
Proof Methodologies for Behavioural Equivalence in DPI.
FORTE
Alberto Ciaffaglione, Matthew Hennessy, Julian Rathke
2003 — —
Certified reasoning on real numbers and objects in co-inductive type theory. (Raisonnement certifié sur les nombres réels et les objets en théorie des types co-inductifs).
Alberto Ciaffaglione
2003 B conf
Imperative Object-Based Calculi in Co-inductive Type Theories.
LPAR
Alberto Ciaffaglione, Luigi Liquori, Marino Miculan
2003 — conf
Plug and Play the Theory of Contexts in Higher-Order Abstract Syntax.
COMETA
Alberto Ciaffaglione, Ivan Scagnetto
2003 — conf
Reasoning on an imperative object-based calculus in Higher Order Abstract Syntax.
MERLIN
Alberto Ciaffaglione, Luigi Liquori, Marino Miculan
2000 — conf
A Tour with Constructive Real Numbers.
TYPES
Alberto Ciaffaglione, Pietro Di Gianantonio
1999 — conf
A Co-inductive Approach to Real Numbers.
TYPES
Alberto Ciaffaglione, Pietro Di Gianantonio