CIAFFAGLIONE, Alberto

CIAFFAGLIONE, Alberto  

DMIF - DIPARTIMENTO DI SCIENZE MATEMATICHE, INFORMATICHE E FISICHE  

Mostra records
Risultati 1 - 14 di 14 (tempo di esecuzione: 0.018 secondi).
Titolo Data di pubblicazione Autore(i) File
A certified, corecursive implementation of exact real numbers 1-gen-2006 Ciaffaglione, Alberto; DI GIANANTONIO, Pietro
A Tour with Constructive Real Numbers 1-gen-2002 Ciaffaglione, Alberto; DI GIANANTONIO, Pietro
A Co-inductive Approach to Real Numbers 1-gen-2000 Ciaffaglione, Alberto; DI GIANANTONIO, Pietro
A definitional implementation of the LAX logical framework LLFP in CoQ, for supporting fast and loose reasoning 1-gen-2019 Alessi, F.; Ciaffaglione, A.; Di Gianantonio, P.; Honsell, F.; Lenisa, M.
Internal Adequacy of Bookkeeping in Coq 1-gen-2014 Ciaffaglione, Alberto; Scagnetto, Ivan
The involutions-as-principal types/ application-as-unification analogy 1-gen-2018 Ciaffaglione, A.; Honsell, F.; Lenisa, M.; Scagnetto, I.
LF+ in Coq for fast-and-loose reasoning 1-gen-2019 Alessi, F; Ciaffaglione, A; Di Gianantonio, P; Honsell, F; Lenisa, M; Scagnetto, I
Mechanizing type environments in weak HOAS 1-gen-2015 Ciaffaglione, Alberto; Scagnetto, Ivan
Plug and Play the Theory of Contexts in Higher-Order abstract Syntax 1-gen-2003 Ciaffaglione, Alberto; Scagnetto, Ivan
Reasoning about Object-based Calculi in (Co)Inductive Type Theory and the Theory of Contexts 1-gen-2007 Ciaffaglione, Alberto; Liquori, L; Miculan, Marino
Reasoning on an Imperative Object-based Calculus in Higher Order Abstract Syntax 1-gen-2003 Ciaffaglione, Alberto; Liquori, Luigi; Miculan, Marino
Revisiting the bookkeeping technique in HOAS-based encodings 1-gen-2013 Ciaffaglione, Alberto; Scagnetto, Ivan
A weak HOAS approach to the POPLmark Challenge 1-gen-2013 Ciaffaglione, Alberto; Scagnetto, Ivan
Λ!-calculus, intersection types, and involutions 1-gen-2019 Ciaffaglione, A.; Di Gianantonio, P.; Honsell, F.; Lenisa, M.; Scagnetto, I.