A Polymorphic Type System for the Lambda-Calculus with Constructors

DOI10.1007/978-3-642-02273-9_18zbMath1218.03018OpenAlexW1603995370MaRDI QIDQ3637198

Barbara Petit

Publication date: 7 July 2009

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-02273-9_18

zbMATH Keywords

polymorphismpattern matchinglambda-calculusstrong normalisation

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Related Items

Unnamed Item, The vectorial \(\lambda\)-calculus

Uses Software

• Coq
• ML
• Haskell
• OCaml

Cites Work

• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Polymorphic type inference and containment
• Locus Solum: From the rules of logic to the logic of rules
• Pure patterns type systems
• The λ-calculus with constructors: Syntax, confluence and separation
• On the Stability by Union of Reducibility Candidates
• Programming Languages and Systems