Alessi, Fabio; Ciaffaglione, Alberto; Di Gianantonio, Pietro; Honsell, Furio; Lenisa, Marina; Scagnetto, Ivan \(\mathrm{LF}^+\) in Coq for fast-and-loose reasoning. (English) Zbl 1427.68344 J. Formaliz. Reason. 12, 11-51 (2019). MSC: 68V15 03B38 03B70 68V20 PDFBibTeX XMLCite \textit{F. Alessi} et al., J. Formaliz. Reason. 12, 11--51 (2019; Zbl 1427.68344) Full Text: DOI
Ciaffaglione, Alberto; Scagnetto, Ivan A weak HOAS approach to the POPLmark challenge. (English) Zbl 1464.68434 Kesner, Delia (ed.) et al., Proceedings of the seventh workshop on logical and semantic frameworks, with applications, Rio de Janeiro, Brazil, September 29–30, 2012. Waterloo: Open Publishing Association (OPA). Electron. Proc. Theor. Comput. Sci. (EPTCS) 113, 109-124 (2013). MSC: 68V20 03B40 03F52 68N15 68V15 PDFBibTeX XMLCite \textit{A. Ciaffaglione} and \textit{I. Scagnetto}, Electron. Proc. Theor. Comput. Sci. (EPTCS) 113, 109--124 (2013; Zbl 1464.68434) Full Text: arXiv Link
Ciaffaglione, Alberto; Liquori, Luigi; Miculan, Marino Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts. (English) Zbl 1118.68046 J. Autom. Reasoning 39, No. 1, 1-47 (2007). MSC: 68N30 03B70 68T15 PDFBibTeX XMLCite \textit{A. Ciaffaglione} et al., J. Autom. Reasoning 39, No. 1, 1--47 (2007; Zbl 1118.68046) Full Text: DOI HAL
Ciaffaglione, Alberto; Di Gianantonio, Pietro A certified, corecursive implementation of exact real numbers. (English) Zbl 1086.68117 Theor. Comput. Sci. 351, No. 1, 39-51 (2006). MSC: 68T15 68Q05 03F60 PDFBibTeX XMLCite \textit{A. Ciaffaglione} and \textit{P. Di Gianantonio}, Theor. Comput. Sci. 351, No. 1, 39--51 (2006; Zbl 1086.68117) Full Text: DOI