Institut de Mathématiques de Luminy


Files &
2001 Vestergaard René and Brotherston James.
A formalised first-order confluence proof for the -calculus using one-sorted variable names (Barendregt was right after all ... almost).
Proceedings of RTA-12, editor : Aart Middeldorp, LNCS 2001, vol. 2051, Springer-Verlag, 2001.
  Vestergaard René and Brotherston James.
The mechanisation of Barendregt-style equational proofs (the residual perspective).
Proceedings of MERLIN-1, Technical report series, Department of Mathematics and Computer Science, University of Leicester, vol. 2001/26, editors : Simon Ambler and Roy Crole and Alberto Momigliano, Collocated with IJCAR, 2001
  Vestergaard René.
The simple type theory of normalisation by evaluation.
Proceedings of WRS-1, Technical report series, Departamento de Sistemas Informáticos y Computación, Universidad Politécnica de Valencia, vol. 2001.2359, editors : Bernhard Gramlich and Salvador Lucas, Collocated with RTA, 2001
  Vestergaard René and Wells J. B.
Cut rules and explicit substitutions (long version).
Math. Structures Comput. Sci., 11(1):131-168, Special issue on explicit substitutions, with selected papers from WESTAPP'99, 2001.
2000 Wells J.B. and Vestergaard René.
Equational reasoning for linking with first-class primitive modules.
Proceedings of ESOP-9, editor : Gert Smolka, vol. 1782, LNCS 2000, Springer Verlag, 2000.
1999 Vestergaard René and Wells J. B.
Cut rules and explicit substitutions (short version).
Proceedings of WESTAPP-2, 1999

1996 Danvy Olivier and Vestergaard René.
Semantics-based compiling: a case study in type-directed partial evaluation.
Proceedings of PLILP-8, editors : Herbert Kuchen and Doaitse Swierstra, LNCS 96, vol. 982, Springer-Verlag, Extended version available as the technical report BRICS-RS-96-13, May 1996.

Last update : july 2, 2001, EL.