35 citations · 105 across the 17 of their papers we have counts for
19 papers
Fixpoint constructions in focused orthogonality models of linear logic
Marcelo Fiore, Zeinab Galal, Farzad Jafarrahmani
Orthogonality is a notion based on the duality between programs and their environments used to determine when they can be safely combined. For instance, it is a powerful tool to es…
Stabilized profunctors and stable species of structures
Marcelo Fiore, Zeinab Galal, Hugo Paquet
We introduce a bicategorical model of linear logic which is a novel variation of the bicategory of groupoids, profunctors, and natural transformations. Our model is obtained by end…
Semantic Analysis of Normalisation by Evaluation for Typed Lambda Calculus
Marcelo Fiore
This paper studies normalisation by evaluation for typed lambda calculus from a categorical and algebraic viewpoint. The first part of the paper analyses the lambda definability re…
Formal Metatheory of Second-Order Abstract Syntax
Marcelo Fiore, Dmitrij Szamozvancev
Despite extensive research both on the theoretical and practical fronts, formalising, reasoning about, and implementing languages with variable binding is still a daunting endeavou…
Free Commutative Monoids in Homotopy Type Theory
Vikraman Choudhury, Marcelo Fiore
We develop a constructive theory of finite multisets in Homotopy Type Theory, defining them as free commutative monoids. After recalling basic structural properties of the free com…
Quotients, inductive types, and quotient inductive types
Marcelo P. Fiore, Andrew M. Pitts, S. C. Steenkamp
This paper introduces an expressive class of indexed quotient-inductive types, called QWI types, within the framework of constructive type theory. They are initial algebras for ind…