Type Theory

  • P.-L.Curien, M.P.Fiore and G.Munch-Maccagnoni.  A Theory of Effects and Resources: Adjunction Models and Polarised Calculi To appear in ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016).  ACM Press, 2016.  [preprint]

  •  
  • M.Devesas Campos and M.P.Fiore.  Classical Logic with Mendler Induction - A Dual Calculus and its Strong Normalization To appear in Symposium on Logical Foundations of Computer Science (LFCS 2016).  Lecture Notes in Computer Science, 2016.  [preprint]   (The final publication will be available at link.sprinker.com.)

  •  
  • M.P.Fiore and O.Mahmoud.  Functorial Semantics of Second-Order Algebraic Theories Arxiv, 2014.  [preprint]

  •  
     
  • M.P.Fiore.  System Fi: a Higher-Order Polymorphic λ-Calculus with Erasable Term-IndicesTalk at the 11th International Conference on Typed Lambda Calculi and Applications.  Eindhoven (The Netherlands), June 2013.  [slides]

  •  
  • M.P.Fiore.  Polymorphic Algebraic TheoriesInvited talk at the GlynnFest Workshop.  Computer Laboratory, University of Cambridge (UK), June 2013.  [slides]

  •  
  • M.P.Fiore and M.Hamana.  Multiversal polymorphic algebraic theories: Syntax, semantics, translations, and equational logicIn Logic in Computer Science Conf. (LICS'13).  IEEE, Computer Society Press, 2013.  [preprint]

  •  
  • K.Y.Ahn, T.Sheard, M.P.Fiore, and A.Pitts.  System Fi: a Higher-Order Polymorphic λ-Calculus with Erasable Term-IndicesIn Proceedings of the 11th International Conference on Typed Lambda Calculi and Applications (TLCA 2013), Lecture Notes in Computer Science, 2013.  [preprint]   [slides]   (The final publication will be available at link.sprinker.com.)

  •  
  • M.P.Fiore.   Discrete Generalised Polynomial FunctorsIn 39th International Colloquium on Automata, Languages and Programming (ICALP 2012), Lecture Notes in Computer Science, Volume 7392, pages 214-226, 2012.  [preprint]   [slides]   (The original publication is available at www.springerlink.com.)

  •  
  • M.P.Fiore.   Second-Order Algebra and Generalised Polynomial FunctorsInvited talk at Algebra and Computation, Logic and Interactions (LI2012), Luminy (France), 2012.  [slides]

  •  
  • M.P.Fiore.   Algebraic Foundations for Type TheoriesTalk given at the 18th Workshop Types for Proofs and Programs (Types 2011), Bergen (Norway), 2011.  [slides]
     
  • M.Hamana and M.P.Fiore.   A Foundation for GADTs and Inductive Families: Dependent Polynomial Functor ApproachTo appear in ACM SIGPLAN 7th Workshop on Generic Programming, 2011.  [preprint]

  •  
  • M.P.Fiore.   On Higher-Order AlgebraInvited talk at the Third Scottish Category Theory Seminar, Glasgow (Scotland), 2010.  [slides]

  •  
  • M.P.Fiore and C.-K.Hur.   Second-order equational logicIn Proceedings of the 19th EACSL Annual Conference on Computer Science Logic (CSL 2010), LNCS 6247, pp. 320-335, 2010.  [preprint]   (The original publication is available at www.springerlink.com.)

  •  
  • M.P.Fiore.   Second-order and dependently-sorted abstract syntaxIn Logic in Computer Science Conf. (LICS'08), pages 57-68.  IEEE, Computer Society Press, 2008.  [preprint] [slides]

  •  
  • M.P.Fiore.   Towards a mathematical theory of substitutionInvited talk at the Annual International Conference on Category Theory, (CT2007), Carvoeiro, Algarve (Portugal), 2007.  [slides]

  •  
  • M.P.Fiore.   A mathematical theory of substitution and its applications to syntax and semanticsInvited tutorial for the Workshop on Mathematical Theories of Abstraction, Substitution and Naming in Computer Science, International Centre for Mathematical Sciences (ICMS), Edinburgh (Scotland), 2007.  [slides]

  •  
  • M.P.Fiore.   Differential structure in models of multiplicative biadditive intuitionistic linear logicIn Typed Lambda Calculi and Applications (TLCA 2007), LNCS 4583, pp. 163-177, 2007.  [preprint]

  •  
  • M.P.Fiore.   On the structure of substitutionInvited address for the 22nd Mathematical Foundations of Programming Semantics Conf. (MFPS XXII), DISI, University of Genova (Italy), 2006.  [2up slides]

  •  
  • M.P.Fiore, R.Di Cosmo and V. Balat. Remarks on isomorphisms in typed lambda calculi with empty and sum typesAnnals of Pure and Applied Logic, Vol. 141, Issues 1-2, pp. 35-50, 2006.  [preprint]  (Extended preliminary version in 17th Logic in Computer Science Conf. (LICS'02), pages 147-156.  IEEE, Computer Society Press, 2002.  [preprint])

  •  
  • M.P.Fiore and T.Leinster.   Isomorphisms on generic mutually recursive polynomial typesInvited talk for the Second International Workshop on Isomorphisms of Types, Toulouse (France), 2005.  [2up slides]

  •  
  • M.P.Fiore and T.Leinster.   A simple description of Thompson's group FPreprint, 2005.  [arXiv]

  •  
  • M.P.Fiore.  Mathematical models of computational and combinatorial structures Invited address for Foundations of Software Science and Computation Structures (FOSSACS 2005), volume 3441 of Lecture Notes in Computer Science, pages 25-46.  Springer-Verlag, 2005.  [pdf preprint] [Springer]

  •  
  • M.P.Fiore and T.Leinster.   Objects of categories as complex numbersAdvances in Mathematics, 190(2): 264-277, 2005.  [arXiv]

  •  
  • M.P.Fiore.  Isomorphisms of generic recursive polynomial types.   In 31st Symposium on Principles of Programming Languages (POPL 2004), pages 77-88.  ACM Press, 2004.  [ps file ]

  •  
  • V.Balat, R.Di Cosmo, and M.P.Fiore.   Extensional normalisation and typed-directed partial evaluation for typed lambda calculus with sums.  In 31st Symposium on Principles of Programming Languages (POPL 2004), pages 64-76.  ACM Press, 2004.  [pdf file ]

  •  
  • M.P.Fiore and T.Leinster.   An objective representation of the Gaussian integersJournal of Symbolic Computation 37(6): 707-716, 2004.  [arXiv]

  •  
  • M.P.Fiore. Semantic analysis of normalisation by evaluation for typed lambda calculus.  In 4th International Conference on Principles and Practice of Declarative Programming (PPDP 2002).  ACM Press, 2002.  [ps file]

  •  
  • M.P.Fiore, G.D.Plotkin and D.Turi. Abstract syntax and variable binding.  In 14th Logic in Computer Science Conf. (LICS'99), pages 193-202.  IEEE, Computer Society Press, 1999.  [ps file]

  •  
  • M.P.Fiore and A.K.Simpson.  Lambda definability with sums via Grothendieck logical relations.  In Proceedings of Typed Lambda Calculi and Applications Conf. (TLCA'99), volume 1581 of Lecture Notes in Computer Science, pages 147-161.  Springer-Verlag, 1999.  [ps file]

  •  
  • M.Abadi and M.P.Fiore.  Syntactic considerations on recursive types.  In 11th Logic in Computer Science Conf. (LICS'96), pages 242-252.  IEEE, Computer Society Press, 1996.  [ps file]

  •  
  • M.P.Fiore.  A coinduction principle for recursive data types based on bisimulation. Information and Computation, 127(2):186-198, 1996.  [ps file]