Type Theory

  • 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]