PreSheaves in Type Theory
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.P.Fiore and C.-K.Hur.
Mathematical Synthesis of Equational Deduction
Systems.
Invited address at the International Conference on
Typed Lambda Calculi and Applications
(TLCA 2009), Brasilia
(Brazil), 2009.
[abstract]
M.P.Fiore and C.-K.Hur.
Term Equational Systems and Logics.
In Proceedings of the 24th Mathematical
Foundations of Programming Semantics Conf.
(MFPS XXIV),
Electronic Notes in Theoretical Computer Science
(ENTCS),
Volume 218, pp. 171-192 , 2008.
[preprint]
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.
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.
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
link]
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.
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]