Publications by Alberto Ciaffaglione

• Mechanizing type environments in weak HOAS (with I. Scagnetto)
  Theoretical Computer Science, volume 606
  Elsevier, 2015
• A Coinductive animation of Turing Machines
  In Proceedings of SBMF 2014, Maceió (Brazil)
  Lecture Notes in Computer Science, volume 8941 - Springer, 2015
• Internal adequacy of bookkeeping in Coq (with I. Scagnetto)
  In Proceedings of LFMTP 2014, Vienna (Austria)
  Article No. 8 - Association for Computing Machinery, 2014
• Revisiting the bookkeeping technique in HOAS-based encodings (with I. Scagnetto)
  In the Book of Abstracts of TYPES 2013, Toulouse (France)
  Institut de Recherche en Informatique de Toulouse, 2013
• A weak HOAS approach to the POPLmark Challenge (with I. Scagnetto)
  In Proceedings of LSFA 2012, Rio de Janeiro (Brazil)
  Electronic Proceedings in Theoretical Computer Science, volume 113 - Open Publishing Association, 2013
• A coinductive semantics of the Unlimited Register Machine
  In Proceedings of INFINITY 2011, Taipei (Taiwan)
  Electronic Proceedings in Theoretical Computer Science, volume 73 - Open Publishing Association, 2011
• About applications of mechanized coinduction
  Technical Report 08/2009
  Department of Mathematics and Computer Science, University of Udine (Italy), 2009
• Reasoning about object-based calculi in (Co)Inductive Type Theory and the Theory of Contexts (with L. Liquori, M. Miculan)
  Journal of Automated Reasoning, volume 39(1)
  Kluwer Academic Publishers, 2007
• A certified, corecursive implementation of exact Real Numbers (with P. Di Gianantonio)
  Theoretical Computer Science, volume 351(1)
  Elsevier, 2006
• Proof methodologies for behavioural equivalence in Distributed pi-calculus. (with M. Hennessy, J. Rathke)
  In Proceedings of FORTE 2005, Taipei (Taiwan) - Best Paper Award
  Lecture Notes in Computer Science, volume 3731 - Springer, 2005
• Plug and play the Theory of Contexts in Higher-Order Abstract Syntax (with I. Scagnetto)
  In Proceedings of COMETA 2003, Udine (Italy)
  Electronic Notes in Theoretical Computer Science, volume 104 - Elsevier, 2004
• Imperative object-based calculi in Coinductive Type Theories (with L. Liquori, M. Miculan)
  In Proceedings of LPAR 2003, Almaty (Kazakhstan)
  Lecture Notes in Artificial Intelligence, volume 2850 - Springer, 2003
• Reasoning on an imperative object-based calculus in Higher-Order Abstract Syntax (with L. Liquori, M. Miculan)
  In Proceedings of MERLIN 2003, Uppsala (Sweden)
  Article No. 4 - Association for Computing Machinery, 2003
• Certified reasoning on Real Numbers and Objects in Coinductive Type Theory
  PhD Thesis Series, Computer Science 2003/1
  Forum, 2003
• Foundations for dynamic object reclassification (with P. Di Gianantonio, F. Honsell, L. Liquori)
  Technical Report 03/2003
  Department of Mathematics and Computer Science, University of Udine (Italy), 2003
• A tour with constructive Real Numbers (with P. Di Gianantonio)
  In Proceedings of TYPES 2000, Durham (United Kingdom)
  Lecture Notes in Computer Science, volume 2277 - Springer, 2002
• A coinductive approach to Real Numbers (with P. Di Gianantonio)
  In Proceedings of TYPES 1999, Lökeberg (Sweden)
  Lecture Notes in Computer Science, volume 1956 - Springer, 2000