44 articles – 42 Notices  [english version]

hal-00578077, version 1

Semantics of Typed Lambda-Calculus with Constructors

Barbara Petit () 1

Logical Methods in Computer Science (LMCS) 7, 1:2 (2011) 1-24

Résumé : We present a Curry-style second-order type system with union and intersection types for the lambda-calculus with constructors of Arbiser, Miquel and Rios, an extension of lambda-calculus with a pattern matching mechanism for variadic constructors. We then prove the strong normalisation and the absence of match failure for a restriction of this system, by adapting the standard reducibility method.

  • 1 :  Laboratoire de l'Informatique du Parallélisme (LIP)
  • Université de Lyon – CNRS : UMR5668 – INRIA – École Normale Supérieure - Lyon – Université Claude Bernard - Lyon I
  • Domaine : Informatique/Théorie et langage formel
  • Mots-clés : lambda-calculus – polymorphism – pattern matching – strong normalisation – reducibility candidates
 
  • hal-00578077, version 1
  • http://hal.archives-ouvertes.fr/hal-00578077
  • oai:hal.archives-ouvertes.fr:hal-00578077
  • Contributeur : Barbara Petit <>
  • Soumis le : Vendredi 18 Mars 2011, 11:55:47
  • Dernière modification le : Vendredi 18 Mars 2011, 11:55:47