A prototype-based approach to object reclassification

Autor: Alberto, Ciaffaglione, Pietro, Di Gianantonio, Furio, Honsell, Luigi, Liquori

We investigate, in the context of functional prototype-based lan- guages, a calculus of objects which might extend themselves upon receiving a message, a capability referred to by Cardelli as a self-inflicted operation. We present a sound type system

Externí odkaz: http://arxiv.org/abs/1808.04190

$\mathsf{LLF}_{\cal P}$: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads

Autor: Furio Honsell, Luigi Liquori, Petar Maksimovic, Ivan Scagnetto

Publikováno v: Logical Methods in Computer Science, Vol Volume 13, Issue 3 (2017)

We extend the constructive dependent type theory of the Logical Framework $\mathsf{LF}$ with monadic, dependent type constructors indexed with predicates over judgements, called Locks. These monads capture various possible proof attitudes in establis

Externí odkaz: https://doaj.org/article/d2e7175eaf0a4b2a993c6cab3345be70

A protoype-based approach to object evolution

Autor: Pietro Di Gianantonio, Luigi Liquori, Alberto Ciaffaglione, Furio Honsell

Publikováno v: The Journal of Object Technology. 20:4:1

We investigate, in the context of functional prototype-based languages , a calculus of objects which might extend themselves upon receiving a message, a possibility referred to by Cardelli as a self-inflicted operation. We present a sound type system

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::a89d64a0791d2a00184b991db928ab6b
https://doi.org/10.5381/jot.2021.20.2.a4

A Decidable Subtyping Logic for Intersection and Union Types

Autor: Luigi Liquori, Claude Stolze

Publikováno v: Lecture Notes in Computer Science
TTCS 2017-2nd International Conference on Topics in Theoretical Computer Science
TTCS 2017-2nd International Conference on Topics in Theoretical Computer Science, Sep 2017, Tehran, Iran. pp.74-90, ⟨10.1007/978-3-319-68953-1_7⟩
Topics in Theoretical Computer Science ISBN: 9783319689524
TTCS

Part 3: Logic, Semantics, and Programming Theory; International audience; Using Curry-Howard isomorphism, we extend the typed lambda-calculus with intersection and union types, and its corresponding proof-functional logic, previously defined by the a

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b9c9785312db63ec59fc9d121baad063
https://hal.inria.fr/hal-01760641/document

Implementing Cantor’s Paradise

Autor: Furio Honsell, Luigi Liquori, Ivan Scagnetto, Marina Lenisa

Publikováno v: Programming Languages and Systems ISBN: 9783319479576
APLAS

Set-theoretic paradoxes have made all-inclusive self-referential Foundational Theories almost a taboo. The few daring attempts in the literature to break this taboo avoid paradoxes by restricting the class of formulae allowed in Cantor’s naive Comp

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::8b608ae103a34b67b0ec5edb54441ac2
https://doi.org/10.1007/978-3-319-47958-3_13