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-Indices.
Talk at the
11th
International Conference on Typed Lambda Calculi and Applications.
Eindhoven (The Netherlands), June 2013.
[slides]
M.P.Fiore.
Polymorphic Algebraic Theories.
Invited 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 logic.
In 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-Indices.
In 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
Functors.
In
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
Functors.
Invited talk at Algebra and Computation, Logic
and Interactions (LI2012),
Luminy (France), 2012.
[slides]
M.P.Fiore.
Algebraic Foundations for Type
Theories.
Talk 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 Approach.
To appear in ACM SIGPLAN 7th Workshop on
Generic Programming, 2011.
[preprint]
M.P.Fiore.
On Higher-Order Algebra.
Invited talk at the Third
Scottish Category Theory Seminar, Glasgow (Scotland),
2010. [slides]
M.P.Fiore and C.-K.Hur.
Second-order equational logic.
In 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
syntax.
In 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
substitution. Invited 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 semantics.
Invited 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 logic.
In Typed Lambda Calculi and Applications
(TLCA 2007),
LNCS 4583, pp. 163-177, 2007.
[preprint]
M.P.Fiore.
On the structure of substitution.
Invited 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 types.
Annals 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 types.
Invited 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
F.
Preprint, 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 numbers.
Advances 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 integers.
Journal 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]