skip to content
Home

Department of Computer Science and Technology

Marcelo Fiore

  • Professor in Mathematical Foundations of Computer Science
  • Fellow of Christ's College

Themes

Teaching

Publications

Journal articles

  • Fiore, M. and Szamozvancev, D., 2022. Formal Metatheory of Second-Order Abstract Syntax PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, v. 6
    Doi: http://doi.org/10.1145/3498715
    •
  • Fiore, M. and Voevodsky, V., 2020. Lawvere theories and C-systems Proceedings of the American Mathematical Society, v. 148
    Doi: http://doi.org/10.1090/proc/14660
    •
  • Devesas Campos, M. and Fiore, M., 2020. Classical logic with Mendler induction Journal of Logic and Computation, v. 30
    Doi: http://doi.org/10.1093/logcom/exaa004
    •
  • Fiore, M., Gambino, N., Hyland, M. and Winskel, G., 2018. Relative pseudomonads, Kleisli bicategories, and substitution monoidal structures Selecta Mathematica, New Series, v. 24
    Doi: http://doi.org/10.1007/s00029-017-0361-3
    •
  • Fiore, MP. and Hur, CK., 2011. On the mathematical synthesis of equational logics Logical Methods in Computer Science, v. 7
    Doi: http://doi.org/10.2168/LMCS-7(3:12)2011
    •
  • Fiore, MP. and Leinster, T., 2010. An abstract characterization of Thompson's group F Semigroup Forum, v. 80
    Doi: http://doi.org/10.1007/s00233-010-9209-2
    •
  • Fiore, MP. and Staton, S., 2009. A congruence rule format for name-passing process calculi Information and Computation, v. 207
    Doi: http://doi.org/10.1016/j.ic.2007.12.005
    •
  • Fiore, MP. and Hur, CK., 2009. On the construction of free algebras for equational systems Theoretical Computer Science, v. 410
    Doi: http://doi.org/10.1016/j.tcs.2008.12.052
    •
  • Fiore, M. and Staton, S., 2009. A congruence rule format for name-passing process calculi INFORM COMPUT, v. 207
    Doi: http://doi.org/10.1016/j.ic.2007.12.005
    •
  • Fiore, MP. and Hur, C-K., 2008. Term Equational Systems and Logics: (Extended Abstract). MFPS, v. 218
    Doi: 10.1016/j.entcs.2008.10.011
    •
  • Fiore, M., Gambino, N., Hyland, M. and Winskel, G., 2008. The cartesian closed bicategory of generalised species of structures J LOND MATH SOC, v. 77
    Doi: http://doi.org/10.1112/jlms/jdm096
    •
  • Fiore, MP., Gambino, N., Hyland, M. and Winskel, G., 2008. The cartesian closed bicategory of generalised species of structures Journal of the London Mathematical Society, v. 77
    Doi: http://doi.org/10.1112/jlms/jdm096
    •
  • Cardelli, L., Fiore, MP. and Winskel, G., 2007. Preface. Computation, Meaning, and Logic, v. 172
    •
  • Cattani, GL. and Fiore, MP., 2007. The Bicategory-Theoretic Solution of Recursive Domain Equations. Computation, Meaning, and Logic, v. 172
    •
  • Fiore, M., Di Cosmo, R. and Balat, V., 2006. Remarks on isomorphisms in typed lambda calculi with empty and sum types ANN PURE APPL LOGIC, v. 141
    Doi: http://doi.org/10.1016/j.apal.2005.09.001
    •
  • Fiore, M. and Staton, S., 2006. Comparing operational models of name-passing process calculi Information and Computation, v. 204
    Doi: http://doi.org/10.1016/j.ic.2005.08.004
    •
  • Fiore, M. and Staton, S., 2006. Comparing operational models of name-passing process calculi INFORMATION AND COMPUTATION, v. 204
    Doi: http://doi.org/10.1016/j.ic.2005.08.004
    •
  • Fiore, M. and Leinster, T., 2005. Objects of categories as complex numbers ADV MATH, v. 190
    Doi: http://doi.org/10.1016/j.aim.2004.01.002
    •
  • Fiore, M. and Staton, S., 2004. Comparing operational models of name-passing process calculi Electronic Notes in Theoretical Computer Science, v. 107
    Doi: http://doi.org/10.1016/j.entcs.2004.02.025
    •
  • Fiore, M. and Leinster, T., 2004. An objective representation of the Gaussian integers J SYMB COMPUT, v. 37
    Doi: http://doi.org/10.1016/jjsc.2003.10.002
    •
  • Fiore, MP. and Leinster, T., 2004. An objective representation of the Gaussian integers. J. Symb. Comput., v. 37
    Doi: 10.1016/j.jsc.2003.10.002
    •
  • Fiore, MP., Moggi, E. and Sangiorgi, D., 2002. A fully abstract model for the pi-calculus INFORM COMPUT, v. 179
    Doi: http://doi.org/10.1006/inco.2002.2968
    •
  • Fiore, MP. and Rosolini, G., 2001. Domains in H. Theor. Comput. Sci., v. 264
    Doi: 10.1016/S0304-3975(00)00221-8
    •
  • Bunge, M. and Fiore, MP., 2000. Unique factorisation lifting functors and categories of linearly-controlled processes. Math. Struct. Comput. Sci., v. 10
    •
  • Fiore, MP., 1999. Fibred models of processes. CTCS, v. 29
    Doi: 10.1016/S1571-0661(05)80307-X
    •
  • Pitelis, C., 1999. Preface Contributions to Political Economy, v. 18
    Doi: http://doi.org/10.1093/cpe/18.1.1
    •
  • Fiore, MP. and Rosolini, G., 1997. The category of cpos from a synthetic viewpoint. MFPS, v. 6
    Doi: 10.1016/S1571-0661(05)80165-3
    •
  • Fiore, MP., 1997. An Enrichment Theorem for an Axiomatisation of Categories of Domains and Continuous Functions. Math. Struct. Comput. Sci., v. 7
    Doi: 10.1017/S0960129597002429
    •
  • Fiore, MP., 1996. A Coinduction Principle for Recursive Data Types Based on Bisimulation. Inf. Comput., v. 127
    Doi: 10.1006/inco.1996.0058
    •
  • Fiore, MP., 1995. Order-Enrichment for Categories of Partial Maps. Math. Struct. Comput. Sci., v. 5
    Doi: 10.1017/S0960129500001225
    •
  • Fiore, MP., On the concrete representation of discrete enriched abstract clones Tbilisi Mathematical Journal, v. 10
    Doi: http://doi.org/10.1515/tmj-2017-0115
    •
  • Fiore, MP., Pitts, AM. and Steenkamp, SC., Quotients, inductive types, and quotient inductive types Logical Methods in Computer Science,
    •
  • Fiore, MP., Analytic functors between presheaf categories over groupoids Theoretical Computer Science, v. 546
    Doi: http://doi.org/10.1016/j.tcs.2014.03.004
    •
  • Fiore, M., Galal, Z. and Paquet, H., Stabilized profunctors and stable species of structures Logical Methods in Computer Science,
    •
  • Fiore, M. and Saville, P., Coherence for bicategorical cartesian closed structure Mathematical Structures in Computer Science,
    •
  • Fiore, M., An Equational Metalogic for Monadic Equational Systems Theory and Applications of Categories,
    •
  • Fiore, M., Semantic Analysis of Normalisation by Evaluation for Typed Lambda Calculus Mathematical Structures in Computer Science,
    Doi: 10.1017/S0960129522000263
    •

    Conference proceedings

  • Fiore, M. and Saville, P., 2020. Coherence and normalisation-by-evaluation for bicategorical cartesian closed structure Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science,
    Doi: http://doi.org/10.1145/3373718.3394769
    •
  • Arkor, N. and Fiore, M., 2020. Algebraic models of simple type theories: A polynomial approach Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science,
    Doi: http://doi.org/10.1145/3373718.3394771
    •
  • Fiore, MP. and Saville, P., 2017. List Objects with Algebraic Structure LIPIcs : Leibniz International Proceedings in Informatics, v. 84
    Doi: http://doi.org/10.4230/LIPIcs.FSCD.2017.16
    •
  • Curien, P-L., Fiore, M. and Munch-Maccagnoni, G., 2016. A theory of effects and resources: adjunction models and polarised calculi Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,
    Doi: 10.1145/2837614.2837652
    •
  • Campos, MD. and Fiore, M., 2016. Classical logic with mendler induction a dual calculus and its strong normalization Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), v. 9537
    Doi: 10.1007/978-3-319-27683-0_4
    •
  • Fiore, M. and Staton, S., 2014. Substitution, jumps, and algebraic effects Proceedings of the Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic, CSL 2014 and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2014,
    Doi: http://doi.org/10.1145/2603088.2603163
    •
  • Ahn, KY., Sheard, T., Fiore, M. and Pitts, AM., 2013. System F<inf>i</inf>: A higher-order polymorphic λ-calculus with erasable term-indices Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), v. 7941 LNCS
    Doi: 10.1007/978-3-642-38946-7_4
    •
  • Fiore, MP., 2012. Discrete Generalised Polynomial Functors - (Extended Abstract). ICALP (2), v. 7392
    •
  • Fiore, MP., 2012. Discrete Generalised Polynomial Functors Lecture Notes in Computer Science, v. 7392
    •
  • Fiore, MP. and Hamana, M., 2011. A Foundation for GADTs and Inductive Families: Dependent Polynomial Functor Approach Proceeding WGP'11 Proceedings of the seventh ACM SIGPLAN workshop on Generic programming,
    Doi: http://doi.org/10.1145/2036918.2036927
    •
  • Fiore, MP. and Mahmoud, O., 2010. Second-order algebraic theories Lecture Notes in Computer Science, v. 6281
    Doi: http://doi.org/10.1007/978-3-642-15155-2_33
    •
  • Fiore, MP. and Hur, CK., 2010. Second-Order Equational Logic Lecture Notes in Computer Science, v. 6247
    Doi: http://doi.org/10.1007/978-3-642-15205-4_26
    •
  • Fiore, MP. and Hur, C-K., 2009. Mathematical Synthesis of Equational Deduction Systems. TLCA, v. 5608
    •
  • Fiore, MP., 2008. Second-order and dependently-sorted abstract syntax Twenty-Third Annual IEEE Symposium on Logic in Computer Science,
    Doi: http://doi.org/10.1109/LICS.2008.38
    •
  • Fiore, MP. and Hur, C-K., 2007. Equational Systems and Free Constructions (Extended Abstract). ICALP, v. 4596
    •
  • Fiore, MP., 2007. Differential structure in models of multiplicative biadditive intuitionistic linear logic Typed Lambda Calculi and Applications, Proceedings, v. 4583
    •
  • Fiore, M. and Staton, S., 2006. A congruence rule format for name-passing process calculi from mathematical structural operational semantics 21st Annual IEEE Symposium on Logic in Computer Science, Proceedings,
    •
  • Fiore, MP., 2005. Mathematical models of computational and combinatorial structures - (Invited address) FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, PROCEEDINGS, v. 3441
    •
  • Fiore, MP., 2005. Mathematical Models of Computational and Combinatorial Structures. FoSSaCS, v. 3441
    •
  • Balat, V., Di Cosmo, R. and Fiore, M., 2004. Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums ACM SIGPLAN NOTICES, v. 39
    •
  • Fiore, M., 2004. Isomorphisms of generic recursive polynomial types ACM SIGPLAN NOTICES, v. 39
    •
  • Fiore, MP., Cosmo, RD. and Balat, V., 2002. Remarks on Isomorphisms in Typed Lambda Calculi with Empty and Sum Types. LICS,
    Doi: 10.1109/LICS.2002.1029824
    •
  • Fiore, MP., 2002. Semantic analysis of normalisation by evaluation for typed lambda calculus. PPDP,
    •
  • Fiore, MP. and Abadi, M., 2001. Computing Symbolic Models for Verifying Cryptographic Protocols. CSFW,
    Doi: 10.1109/CSFW.2001.930144
    •
  • Fiore, MP. and Turi, D., 2001. Semantics of Name and Value Passing. LICS,
    Doi: 10.1109/LICS.2001.932486
    •
  • Fiore, MP., 2000. Fibred Models of Processes: Discrete, Continuous, and Hybrid Systems. IFIP TCS, v. 1872
    •
  • Fiore, MP., Cattani, GL. and Winskel, G., 1999. Weak Bisimulation and Open Maps. LICS,
    Doi: 10.1109/LICS.1999.782590
    •
  • Fiore, MP. and Simpson, AK., 1999. Lambda Definability with Sums via Grothendieck Logical Relations. TLCA, v. 1581
    •
  • Fiore, MP., Plotkin, GD. and Turi, D., 1999. Abstract Syntax and Variable Binding. LICS,
    Doi: 10.1109/LICS.1999.782615
    •
  • Cattani, GL., Fiore, M. and Winskel, G., 1998. A theory of recursive domains with applications to concurrency THIRTEENTH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS,
    •
  • Fiore, MP. and Honda, K., 1998. Recursive Types in Games: Axiomatics and Process Representation. LICS,
    Doi: 10.1109/LICS.1998.705670
    •
  • Fiore, MP., Plotkin, GD. and Power, AJ., 1997. Complete Cuboidal Sets in Axiomatic Domain Theory. LICS,
    Doi: 10.1109/LICS.1997.614954
    •
  • Abadi, M. and Fiore, MP., 1996. Syntactic Considerations on Recursive Types. LICS,
    Doi: 10.1109/LICS.1996.561324
    •
  • Fiore, MP. and Plotkin, GD., 1996. An Extension of Models of Axiomatic Domain Theory to Models of Synthetic Domain Theory. CSL, v. 1258
    •
  • Fiore, MP., Moggi, E. and Sangiorgi, D., 1996. A Fully-Abstract Model for the pi-Calculus (Extended Abstract). LICS,
    Doi: 10.1109/LICS.1996.561302
    •
  • Fiore, MP., 1995. Lifting as a KZ-Doctrine. Category Theory and Computer Science, v. 953
    •
  • Fiore, MP. and Plotkin, GD., 1994. An Axiomatization of Computationally Adequate Domain Theoretic Models of FPC LICS,
    Doi: 10.1109/LICS.1994.316083
    •
  • Fiore, MP., 1993. A Coinduction Principle for Recursive Data Types Based on Bisimulation LICS,
    Doi: 10.1109/LICS.1993.287595
    •
  • Fiore, M. and Choudhury, V., Free Commutative Monoids in Homotopy Type Theory Electronic Notes in Theoretical Informatics and Computer Science, v. Volume 1 - Proceedings of MFPS XXXVIII
    Doi: http://doi.org/10.46298/entics.10492
    •
  • Fiore, MP. and Devesas Campos, M., The Algebra of Directed Acyclic Graphs Lecture Notes in Computer Science, v. 7860
    Doi: http://doi.org/10.1007/978-3-642-38164-5_4
    •
  • Fiore, M., Galal, Z. and Jafarrahmani, F., Fixpoint constructions in focused orthogonality models of linear logic Proceedings of MFPS 2023, Electronic Notes in Theoretical Informatics And Computer Science,
    Doi: http://doi.org/10.46298/entics.12302
    •
  • Pitts, A., Fiore, M. and Steenkamp, S., Constructing Infinitary Quotient-Inductive Types Springer Lecture Notes in Computer Science,
    •
  • Fiore, M. and Szamozvancev, D., Formal Metatheory of Second-Order Abstract Syntax
  • Fiore, M., Galal, Z. and Paquet, H., A combinatorial approach to higher-order structure for polynomial functors LIPIcs – Leibniz International Proceedings in Informatics, v. 228
    Doi: 10.4230/LIPIcs.FSCD.2022.31
    •
  • Ahn, KY., Sheard, T., Fiore, MP. and Pitts, AM., System Fi Lecture Notes in Computer Science, v. 7941
    •
  • Fiore, M. and Saville, P., Relative full completeness for bicategorical cartesian closed structure
    Doi: http://doi.org/10.1007/978-3-030-45231-5_15
    •

    Book chapters

  • Fiore, M. and Saville, P., 2020. Relative Full Completeness for Bicategorical Cartesian Closed Structure
    Doi: http://doi.org/10.1007/978-3-030-45231-5_15
    •

    Working papers

  • Fiore, M., 2015. An Axiomatics and a Combinatorial Model of Creation/Annihilation Operators

    • Theses / dissertations

  • Elsayed, OM., 2011. Second-Order Algebraic Theories
    Doi: http://doi.org/10.17863/CAM.16369
    •
  • Arkor, N., Monadic and Higher-Order Structure

    • Internet publications

  • Fiore, M., Galal, Z. and Paquet, H., Stabilized profunctors and stable species of structures

    • Datasets

  • Fiore, M., Pitts, A. and Steenkamp, S., Code supporting "Constructing Infinitary Quotient-Inductive Types"
  • Pitts, A., Steenkamp, S. and Fiore, M., Agda code supporting "Quotients, Inductive Types and Quotient Inductive Types"
  • Pitts, A., Fiore, M. and Steenkamp, SC., Agda code supporting "Quotients, Inductive Types and Quotient Inductive Types" (v2)

    • Contact Details

    Room: 
    FE19
    Office phone: 
    (01223) 3-34622
    Email: 

    marcelo.fiore@cl.cam.ac.uk

    Contact us

    Department of Computer Science and Technology
    University of Cambridge
    William Gates Building
    15 JJ Thomson Avenue
    Cambridge
    CB3 0FD

    Information provided by pagemaster@cst.cam.ac.uk

    Privacy policy

    Social media

    Athena Swan bronze award logo

    Study at Cambridge

    About the University

    Research at Cambridge