Publications of Gilles Barthe
Back to my home page.
Papers
-
G. Barthe. Extensions
of pure type systems. In M. Dezani-Ciancaglini and G. Plotkin, editors,
Proceedings of TLCA'95, LNCS 902, pp 16--31.
-
G. Barthe.
A
simple abstract semantics for equational theories. In H. Reichel, editor,
Proceedings of FCT'95, LNCS 965, pp 126--135.
-
G. Barthe and H. Geuvers. Modular properties of algebraic type systems. In
G. Dowek, J. Heering, K. Meinke and B. Möller, editors,
Proceedings of HOA'95, LNCS 1074, pp 37--56.
-
G. Barthe and H. Geuvers. Congruence types. In H. Kleine Buening, editor, Proceedings of
CSL'95 , LNCS 1092, pp 36--51.
-
G. Barthe. Implicit coercions in type systems. In S. Berardi and M. Coppo, editors,
Proceedings of Types'95, LNCS 1128, pp 1--15.
-
G. Barthe, M. Ruys and H. Barendregt. A
two-level approach towards lean proof-checking. In S. Berardi and M.
Coppo, editors, Proceedings of Types'95, LNCS 1128, pp 16--35.
-
G. Barthe and P.-A. Melliès. On the subject reduction property for algebraic type systems. In D. van
Dalen and M. Bezem, editors, Proceedings of CSL'96, LNCS 1258, pp
34--57.
-
G. Barthe, J. Hatcliff and M.H. Sørensen. A
notion of classical pure type system (preliminary report). In S. Brookes
and M. Mislove, editors, Proceedings of MFPS'97, ENTCS volume 6.
-
G. Barthe, J. Hatcliff and M.H. Sørensen. Reflections
on reflections. In H. Glaser, P. Hartel and H. Kuchen, editors, Proceedings
of PLILP'97, LNCS 1292, pp 241--258.
-
G. Barthe and F. van Raamsdonk. Termination
of algebraic type systems: the syntactic approach. In M. Hanus and
J. Heering, editors, Proceedings of ALP'97, LNCS 1298, pp 174--193.
(This is a preliminary version.)
-
G. Barthe, F. Kamareddine and A. Ríos. Explicit
substitutions for the lambda-delta calculus. In M. Hanus and J. Heering,
editors, Proceedings of ALP'97, LNCS 1298, pp 209--223.
-
G. Barthe, J. Hatcliff and P. Thiemann. Monadic
Type Systems: Pure Type Systems for Impure Settings (Preliminary Report).
In Proceedings of HOOTS'97, ENTCS volume 10.
-
G. Barthe.
The relevance of proof-irrelevance. In K. Larsen, S. Skyum and G. Winskel,
editors, Proceedings of ICALP'98, LNCS 1443, pp 755--768.
-
G. Barthe.
The semi-full closure of Pure Type Systems. In L. Brim, J. Gruska and J.
Zlatuska, editors, Proceedings of MFCS'98, LNCS 1450, pp 316--325.
-
G. Barthe. Existence and Uniqueness of Normal Forms in Pure Type Systems with beta-eta
conversion.
In G. Gottlob, E. Grandjean and K. Seyr, editors, Proceedings of CSL'98,
LNCS 1584, pp 241--259.
-
G. Barthe. Order-sorted inductive types. In Information and
Computation, 149(1):42-76, February 1999.
-
G. Barthe. Expanding the cube. In W. Thomas, editor,
Proceedings of FOSSACS'99, LNCS 1578,
pp 90--103.
-
G. Barthe and M.J. Frade.
Constructor subtyping. In D. Swiestra, editor, Proceedings of
ESOP'99, LNCS 1576, pp 109--127.
-
G. Barthe, J. Hatcliff and M.H. Sørensen. CPS translations and applications: the Cube and beyond. In Higher
Order and Symbolic Computation, 12(2):125--170, September 1999.
A preliminary version appears in O. Danvy, editor, Proceedings of the
second ACM SIGPLAN workshop on Continuations, Paris, France,
January 1997.
- G. Barthe.
Type-checking Injective Pure Type Systems. In
Journal of Functional Programming 9(6):675--698,
November 1999.
- G. Barthe and F. van Raamsdonk.
Constructor Subtyping in the Calculus of Inductive
Constructions. In J. Tiuryn, editor, Proceedings of
FOSSACS'00, LNCS 1784, pp 17--34.
-
G. Barthe and M.H. Sørensen. Domain-free pure type systems. In Journal of
Functional Programming, 10(5):412--452, September 2000. A
preliminary version appears in S. Adian and A. Nerode, editors,
Proceedings of LFCS'97, LNCS 1234. pp 9--20.
- G. Barthe and O. Pons. Type Isomorphisms and Proof Reuse in Dependent Type
Theory. In F. Honsell and M. Miculan, editors, Proceedings
of FOSSACS'01, LNCS 2030, pp 57--71.
- G. Barthe, J. Hatcliff and M.H. Sørensen.
An induction principle for Pure Type Systems. In
Theoretical Computer Science, 266(1/2):773--818, September 2001.
-
G. Barthe, J. Hatcliff and M.H. Sørensen.
Weak Normalization Implies Strong Normalization in
Generalized Non-Dependent Pure Type Systems. In
Theoretical Computer Science, 269(1/2):317--361, October 2001.
-
G. Barthe and T. Uustalu.
CPS Translating Inductive and Coinductive Types. In
P. Thiemann, editor, Proceedings of PEPM'02, ACM Press, 2002.
- G. Barthe, V. Capretta and O. Pons.
Setoids in type theory. In Journal of Functional Programming,
13(2):261-293, March 2003.
- G. Barthe and T. Coquand.
An Introduction to Dependent Type Theory. In G. Barthe,
P. Dybjer, L. Pinto, and J. Saraiva, editors, Proceedings
of APPSEM'00, LNCS 2395, pp 1--41.
- G. Barthe, M. J. Frade, E. Giménez, L. Pinto and
T. Uustalu.
Type-based termination of recursive definitions. In Mathematical Structures in Computer Science. To appear.
- G. Barthe and T. Coquand.
On the equational theory of non normalising Pure Type Systems.
In Journal of Functional Programming,
to appear.
- G. Barthe, H. Cirstea, C. Kirchner and L. Liquori.
Pure Pattern Type Systems. In G. Morrisett, Proceedings of POPL'03, ACM Press.