Author

Marcelo Fiore

90 papers · 1995–2026

1995peak 8 in 20022026

Frequent co-authors

Papers

showing 1–25 of 90 RSS

Abstract syntax and variable binding

Marcelo Fiore, Gordon Plotkin, Daniele Turi

Artificial Intelligence · Figshare · 20 Jan 2003 · cited 359× · DOI ↗ · more like this ·

We develop a theory of abstract syntax with variable binding. To every binding signature we associate a category of models consisting of variable sets endowed with compatible algebra and substitution structures. The syntax generated by the signature is the initial model. This gives a notion of initial algebra semantics encompassing the traditional one; besides compositionality, it automatically verifies the semantic substitution lemma.

Semantic Analysis of Normalisation by Evaluation for Typed Lambda Calculus

Marcelo Fiore

cs.LO · July 2022 · cited 112× · arXiv ↗ · more like this ·

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 result of Jung and Tiuryn via Kripke logical relations and shows how it can be adapted to unify definability and normalisation, yielding an extensional normalisation result. In the second part of the paper the analysis is refined further by considering intensional Kripke relations (in the form of Artin glueing) and shown to provide a function for normalising terms, casting normalisation by evaluation in the context of categorical glueing. The technical development includes an algebraic treatment of the syntax and semantics of the typed lambda calculus that allows the definition of the normalisation function to be given within a simply typed metatheory. A normalisation-by-evaluation program in a dependently-typed…

The cartesian closed bicategory of generalised species of structures

Marcelo Fiore, Nicola Gambino, Martin Hyland +1 more

Mathematical Physics · Journal of the London Mathematical Society · 20 Oct 2007 · cited 99× · DOI ↗ · more like this ·

The concept of generalised species of structures between small categories and, correspondingly, that of generalised analytic functor between presheaf categories are introduced. An operation of substitution for generalised species, which is the counterpart to the composition of generalised analytic functors, is also put forward. These definitions encompass most notions of combinatorial species considered in the literature — including of course Joyal's original notion — together with their associated substitution operation. Our first main result exhibits the substitution calculus of generalised species as arising from a Kleisli bicategory for a pseudo-comonad on profunctors. Our second main result establishes that the bicategory of generalised species of structures is cartesian closed.

Computing symbolic models for verifying cryptographic protocols

Marcelo Fiore, M. Abadi

Computer Networks and Communications · 2001 · cited 87× · DOI ↗ · more like this ·

We consider the problem of automatically verifing infinite-state cryptographic protocols. Specifically, we present an algorithm that given a finite process describing a protocol in a hostile environment (trying to force the system into a "bad" state) computes a model of traces on which security properties can be checked. Because of unbounded inputs from the environment, even finite processes have an infinite set of traces: the main focus of our approach is the reduction of this infinite set to a finite set by a symbolic analysis of the knowledge of the environment. Our algorithm is sound (and we conjecture complete) for protocols with shared-key encryption-decryption that use arbitrary messages as keys; further it is complete in the common and important case in which the cryptographic keys are messages of bounded size.

Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums

Vincent Balat, Roberto Di Cosmo, Marcelo Fiore

Artificial Intelligence · HAL (Le Centre pour la Communication Scientifique Directe) · 2004 · cited 79× · DOI ↗ · more like this ·

We present a notion of η-long β-normal term for the typed lambda calculus with sums and prove, using Grothendieck logical relations, that every term is equivalent to one in normal form. Based on this development we give the first type-directed partial evaluator that constructs %able to construct normal forms of terms in this calculus.

An axiomatisation of computationally adequate domain theoretic models of FPC

Marcelo Fiore, Gordon Plotkin

Artificial Intelligence · ERA · 17 Dec 2002 · cited 77× · DOI ↗ · more like this ·

Categorical models of the metalanguage FPC (a type theory with sums, products, exponentials and recursive types) are defined. Then, domain-theoretic models of FPC are axiomatised and a wide subclass of them-the absolute ones-are proved to be both computationally sound and adequate. Examples include: the category of cpos and partial continuous functions and functor categories over it.< <ETX xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">></ETX>

Second-Order and Dependently-Sorted Abstract Syntax

Marcelo Fiore

Artificial Intelligence · Proceedings - Symposium on Logic in Computer Science · June 2008 · cited 59× · DOI ↗ · more like this ·

The paper develops a mathematical theory in the spirit of categorical algebra that provides a model theory for second-order and dependently-sorted syntax. The theory embodies notions such as alpha-equivalence, variable binding, capture-avoiding simultaneous substitution, term metavariable, meta-substitution, mono and multi sorting, and sort dependency. As a matter of illustration, a model is used to extract a second-order syntactic theory, which is thus guaranteed to be correct by construction.

Syntactic considerations on recursive types

M. Abadi, Marcelo Fiore

Artificial Intelligence · 23 Dec 2002 · cited 58× · DOI ↗ · more like this ·

We study recursive types from a syntactic perspective. In particular, we compare the formulations of recursive types that are used in programming languages and formal systems. Our main tool is a new syntactic explanation of type expressions as functors. We also introduce a simple logic for programs with recursive types in which we carry out our proofs.

Relative pseudomonads, Kleisli bicategories, and substitution monoidal structures

Marcelo Fiore, Nicola Gambino, Martin Hyland +1 more

math.CT · December 2016 · cited 51× · arXiv ↗ · more like this ·

We introduce the notion of a relative pseudomonad, which generalises the notion of a pseudomonad, and define the Kleisli bicategory associated to a relative pseudomonad. We then present an efficient method to define pseudomonas on the Kleisli bicategory of a relative pseudomonad. The results are applied to define several pseudomonads on the bicategory of profunctors in an homogeneous way, thus providing a uniform approach to the definition of bicategories that are of interest in operad theory, mathematical logic, and theoretical computer science.

Weak bisimulation and open maps

Marcelo Fiore, Gian Luca Cattani, Glynn Winskel

Computational Theory and Mathematics · 20 Jan 2003 · cited 48× · DOI ↗ · more like this ·

A systematic treatment of weak bisimulation and observational congruence on presheaf models is presented. The theory is developed with respect to a "hiding" functor from a category of paths to observable paths. Via a view of processes as bundles, we are able to account for weak morphisms (roughly only required to preserve observable paths) and to derive a saturation monad (on the category of presheaves over the category of paths). Weak morphisms may be encoded as strong ones via the Kleisli construction associated to the saturation monad. A general notion of weak open-map bisimulation is introduced, and results relating various notions of strong and weak bisimulation are provided. The abstract theory is accompanied by fine concrete study of two key models for concurrency, the interleaving model of synchronisation trees and the independence model of labelled event structures.

A theory of recursive domains with applications to concurrency

Gian Luca Cattani, Marcelo Fiore, Glynn Winskel

Artificial Intelligence · 27 Nov 2002 · cited 48× · DOI ↗ · more like this ·

We develop a 2-categorical theory for recursively defined domains. In particular we generalise the traditional approach based on order-theoretic structures to category-theoretic ones. A motivation for this development is the need of a domain theory for concurrency, with an account of bisimulation. Indeed, the leading examples throughout the paper are provided by recursively defined presheaf models for concurrent process calculi. Further we use the framework to study (open-map) bisimulation.

A fully-abstract model for the π-calculus

Marcelo Fiore, Eugenio Moggi, Davide Sangiorgi

Artificial Intelligence · 23 Dec 2002 · cited 46× · DOI ↗ · more like this ·

This paper provides both a fully abstract (domain-theoretic) model for the /spl pi/-calculus and a universal (set-theoretic) model for the finite /spl pi/-calculus with respect to strong late bisimulation and congruence. This is done by: considering categorical models, defining a metalanguage for these models, and translating the /spl pi/-calculus into the metalanguage. A technical novelty of our approach is an abstract proof of full abstraction: The result on full abstraction for the finite /spl pi/-calculus in the set-theoretic model is axiomatically extended to the whole /spl pi/-calculus with respect to the domain-theoretic interpretation. In this proof, a central role is played by the description of non-determinism as a free construction and by the equational theory of the metalanguage.

Abstract Syntax and Variable Binding (Extended Abstract)

Marcelo Fiore, Gordon Plotkin, Daniele Turi

Artificial Intelligence · ERA · 6 Nov 2003 · cited 42× · OpenAlex ↗ · more like this ·

Abstract We develop a theory of abstract syntax with variable binding. To every binding signature we associate a category of models consisting of variable sets endowed with both a (binding) algebra and a substitution structure compatible with each other. The syntax generated by the signature is the initial model. This gives a notion of initial algebra semantics encompassing the traditional one; besides compositionality, it automatically verifies the semantic substitution lemma.

A Congruence Rule Format for Name-Passing Process Calculi from Mathematical Structural Operational Semantics

Marcelo Fiore, Sam Staton

Artificial Intelligence · 22 Sep 2006 · cited 36× · DOI ↗ · more like this ·

We introduce a mathematical structural operational semantics that yields a congruence result for bisimilarity and is suitable for investigating rule formats for name-passing systems. Indeed, we instantiate this general abstract model theory in a framework of nominal sets and extract from it a GSOS-like rule format for name-passing process calculi for which the associated notion of behavioural equivalence - given by a form of open bisimilarity - is a congruence

Term Equational Systems and Logics

Marcelo Fiore, Chung-Kil Hur

Artificial Intelligence · Electronic Notes in Theoretical Computer Science · October 2008 · cited 33× · DOI ↗ · more like this ·

We introduce an abstract general notion of system of equations between terms, called Term Equational System, and develop a sound logical deduction system, called Term Equational Logic, for equational reasoning. Further, we give an analysis of algebraic free constructions that together with an internal completeness result may be used to synthesise complete equational logics. Indeed, as an application, we synthesise a sound and complete nominal equational logic, called Synthetic Nominal Equational Logic, based on the category of Nominal Sets.

A theory of effects and resources: adjunction models and polarised calculi

Pierre-Louis Curien, Marcelo Fiore, Guillaume Munch-Maccagnoni

Artificial Intelligence · Apollo (University of Cambridge) · 7 Jan 2016 · cited 30× · DOI ↗ · more like this ·

We consider the Curry-Howard-Lambek correspondence for effectful computation and resource management, specifically proposing polarised calculi together with presheaf-enriched adjunction models as the starting point for a comprehensive semantic theory relating logical systems, typed calculi, and categorical models in this context. Our thesis is that the combination of effects and resources should be considered orthogonally. Model theoretically, this leads to an understanding of our categorical models from two complementary perspectives: (i) as a linearisation of CBPV (Call-by-Push-Value) adjunction models, and (ii) as an extension of linear/non-linear adjunction models with an adjoint resolution of computational effects. When the linear structure is cartesian and the resource structure is trivial we recover Levy’s notion of CBPV adjunction model, while when the effect structure is…

Formal Metatheory of Second-Order Abstract Syntax

Marcelo Fiore, Dmitrij Szamozvancev

cs.LO · 10 Jan 2022 · cited 29× · arXiv ↗ · more like this ·

Despite extensive research both on the theoretical and practical fronts, formalising, reasoning about, and implementing languages with variable binding is still a daunting endeavour - repetitive boilerplate and the overly complicated metatheory of capture-avoiding substitution often get in the way of progressing on to the actually interesting properties of a language. Existing developments offer some relief, however at the expense of inconvenient and error-prone term encodings and lack of formal foundations. We present a mathematically-inspired language-formalisation framework implemented in Agda. The system translates the description of a syntax signature with variable-binding operators into an intrinsically-encoded, inductive data type equipped with syntactic operations such as weakening and substitution, along with their correctness properties. The generated metatheory further…

Isomorphisms of generic recursive polynomial types

Marcelo Fiore

Artificial Intelligence · 2004 · cited 26× · DOI ↗ · more like this ·

This paper gives the first decidability results on type isomorphism for recursive types, establishing the explicit decidability of type isomorphism for the type theory of sums and products over an inhabited generic recursive polynomial type. The technical development provides connections between themes in programming-language theory (type isomorphism) and computational algebra (Gröbner bases).

Remarks on isomorphisms in typed lambda calculi with empty and sum types

Marcelo Fiore, Roberto Di Cosmo, Vincent Balat

Artificial Intelligence · HAL (Le Centre pour la Communication Scientifique Directe) · 25 Jun 2003 · cited 24× · DOI ↗ · more like this ·

Tarski asked whether the arithmetic identities taught in high school are complete for showing all arithmetic equations valid for the natural numbers. The answer to this question for the language of arithmetic expressions using a constant for the number one and the operations of product and exponentiation is affirmative, and the complete equational theory also characterises isomorphism in the typed lambda calculus, where the constant for one and the operations of product and exponentiation respectively correspond to the unit type and the product and arrow type constructors. This paper studies isomorphisms in typed lambda calculi with empty and sum types from this viewpoint. We close an open problem by establishing that the theory of type isomorphisms in the presence of product, arrow, and sum types (with or without the unit type) is not finitely axiomatisable. Further, we observe that…

Complete cuboidal sets in axiomatic domain theory

Marcelo Fiore, Gordon Plotkin, John Power

Artificial Intelligence · 22 Nov 2002 · cited 20× · DOI ↗ · more like this ·

We study the enrichment of models of axiomatic domain theory. To this end, we introduce a new and broader notion of domain, via, that of complete cuboidal set, that complies with the axiomatic requirements. We show that the category of complete cuboidal sets provides a general notion of enrichment for a wide class of axiomatic domain-theoretic structures.

Substitution, jumps, and algebraic effects

Marcelo Fiore, Sam Staton

Artificial Intelligence · Radboud Repository (Radboud University) · 14 Jul 2014 · cited 17× · DOI ↗ · more like this ·

Algebraic structures abound in programming languages. The starting point for this paper is the following theorem: (first-order) algebraic signatures can themselves be described as free algebras for a (second-order) algebraic theory of substitution. Transporting this to the realm of programming languages, we investigate a computational metalanguage based on the theory of substitution, demonstrating that substituting corresponds to jumping in an abstract machine. We use the theorem to give an interpretation of a programming language with arbitrary algebraic effects into the metalanguage with substitution/jumps.

A foundation for GADTs and inductive families

Makoto Hamana, Marcelo Fiore

Artificial Intelligence · 18 Sep 2011 · cited 17× · DOI ↗ · more like this ·

Every Algebraic Datatype (ADT) is characterised as the initial algebra of a polynomial functor on sets. This paper extends the characterisation to the case of more advanced datatypes: Generalised Algebraic Datatypes (GADTs) and Inductive Families. Specifically, we show that GADTs and Inductive Families are characterised as initial algebras of dependent polynomial functors. The theoretical tool we use throughout is an abstract notion of polynomial between sets together with its associated general form of polynomial functor between categories of indexed sets introduced by Gambino and Hyland.

Unique factorisation lifting functors and categories of linearly-controlled processes

Marta Bunge, Marcelo Fiore

Mathematical Physics · Mathematical Structures in Computer Science · April 2000 · cited 17× · DOI ↗ · more like this ·

We consider processes consisting of a category of states varying over a control category as prescribed by a unique factorisation lifting functor. After a brief analysis of the structure of general processes in this setting, we restrict attention to linearly-controlled ones. To this end, we introduce and study a notion of path-linearisable category in which any two paths of morphisms with equal composites can be linearised (or interleaved) in a canonical fashion. Our main result is that categories of linearly-controlled processes ( viz ., processes controlled by path-linearisable categories) are sheaf models.

Quotients, inductive types, and quotient inductive types

Marcelo P. Fiore, Andrew M. Pitts, S. C. Steenkamp

cs.LO · January 2021 · cited 16× · arXiv ↗ · more like this ·

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 indexed families of equational theories with possibly infinitary operators and equations. We prove that QWI types can be derived from quotient types and inductive types in the type theory of toposes with natural number object and universes, provided those universes satisfy the Weakly Initial Set of Covers (WISC) axiom. We do so by constructing QWI types as colimits of a family of approximations to them defined by well-founded recursion over a suitable notion of size, whose definition involves the WISC axiom. We developed the proof and checked it using the Agda theorem prover.

A type theory for cartesian closed bicategories (Extended Abstract)

Marcelo Fiore, Philip Saville

Artificial Intelligence · Edinburgh Research Explorer · June 2019 · cited 13× · DOI ↗ · more like this ·

We construct an internal language for cartesian closed bicategories. Precisely, we introduce a type theory modelling the structure of a cartesian closed bicategory and show that its syntactic model satisfies an appropriate universal property, thereby lifting the Curry-Howard-Lambek correspondence to the bicategorical setting. Our approach is principled and practical. Weak substitution structure is constructed using a bicategori-fication of the notion of abstract clone from universal algebra, and the rules for products and exponentials are synthesised from semantic considerations. The result is a type theory that employs a novel combination of 2-dimensional type theory and explicit substitution, and directly generalises the Simply-Typed Lambda Calculus. This work is the first step in a programme aimed at proving coherence for cartesian closed bicategories.