A Co-inductive Approach to Real Numbers. - Alberto Ciaffaglione; Pietro Di Gianantonio (TYPES, 1999)

A Tour with Constructive Real Numbers. - Alberto Ciaffaglione; Pietro Di Gianantonio (TYPES, 2000)

Reasoning on an imperative object-based calculus in Higher Order Abstract Syntax. - Alberto Ciaffaglione; Luigi Liquori; Marino Miculan (MERLIN, 2003)

Imperative Object-Based Calculi in Co-inductive Type Theories. - Alberto Ciaffaglione; Luigi Liquori; Marino Miculan (LPAR, 2003)

Plug and Play the Theory of Contexts in Higher-Order Abstract Syntax. - Alberto Ciaffaglione; Ivan Scagnetto (COMETA, 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)

Proof Methodologies for Behavioural Equivalence in DPI. - Alberto Ciaffaglione; Matthew Hennessy; Julian Rathke (FORTE, 2005)

A certified, corecursive implementation of exact real numbers. - Alberto Ciaffaglione; Pietro Di Gianantonio (Theor. Comput. Sci., 2006)

Reasoning about Object-based Calculi in (Co)Inductive Type Theory and the Theory of Contexts. - Alberto Ciaffaglione; Luigi Liquori; Marino Miculan (J. Autom. Reason., 2007)

A coinductive semantics of the Unlimited Register Machine - Alberto Ciaffaglione (INFINITY, 2011)

A weak HOAS approach to the POPLmark Challenge - Alberto Ciaffaglione; Ivan Scagnetto (LSFA, 2012)

Internal Adequacy of Bookkeeping in Coq. - Alberto Ciaffaglione; Ivan Scagnetto (LFMTP, 2014)

A Coinductive Animation of Turing Machines. - Alberto Ciaffaglione (SBMF, 2014)

Mechanizing type environments in weak HOAS. - Alberto Ciaffaglione; Ivan Scagnetto (Theor. Comput. Sci., 2015)

Towards Turing computability via coinduction. - Alberto Ciaffaglione (Sci. Comput. Program., 2016)

The involutions-as-principal types/application-as-unification Analogy. - Alberto Ciaffaglione; Furio Honsell; Marina Lenisa; Ivan Scagnetto (LPAR, 2018)

Linear lambda-calculus and Reversible Automatic Combinators. - Alberto Ciaffaglione; Furio Honsell; Marina Lenisa; Ivan Scagnetto (CoRR, 2018)

A prototype-based approach to object reclassification. - Alberto Ciaffaglione; Pietro Di Gianantonio; Furio Honsell; Luigi Liquori (CoRR, 2018)

lambda!-calculus, Intersection Types, and Involutions. - Alberto Ciaffaglione; Pietro Di Gianantonio; Furio Honsell; Marina Lenisa; Ivan Scagnetto (FSCD, 2019)

A Definitional Implementation of the Lax Logical Framework LLFP in Coq, for Supporting Fast and Loose Reasoning. - Fabio Alessi; Alberto Ciaffaglione; Pietro Di Gianantonio; Furio Honsell; Marina Lenisa (LFMTP@LICS, 2019)

LF+ in Coq for "fast and loose" reasoning. - Fabio Alessi; Alberto Ciaffaglione; Pietro Di Gianantonio; Furio Honsell; Marina Lenisa; Ivan Scagnetto (J. Formaliz. Reason., 2019)

A protoype-based approach to object evolution. - Alberto Ciaffaglione; Pietro Di Gianantonio; Furio Honsell; Luigi Liquori (J. Object Technol., 2021)