Pure patterns type systems

DOI10.1145/604131.604152MaRDI QIDQ2942930zbMATH OpenOpenAlexFDO

Authors Gilles Barthe, Horatiu Cirstea, Claude Kirchner, Luigi Liquori

Publication date 11 September 2015

Published in Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://hal.inria.fr/inria-00099463v2/file/2003-popl-03.pdf

zbMATH Keywords

Curry-Howardlambda-calculuslogicsmatchingpatternspure type systemsrewriting

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Grammars and rewriting systems (68Q42)

Recommendations

• Strong normalisation in two Pure Pattern Type Systems
• scientific article; zbMATH DE number 2163051
• Pure type systems in rewriting logic: specifying typed higher-order languages in a first-order logical framework
• Pattern matching as cut elimination
• A typed pattern calculus

Cites work

• scientific article; zbMATH DE number 3511563 (Why is no real title available?)
• scientific article; zbMATH DE number 615137 (Why is no real title available?)
• scientific article; zbMATH DE number 1942450 (Why is no real title available?)
• scientific article; zbMATH DE number 1948151 (Why is no real title available?)
• scientific article; zbMATH DE number 1953123 (Why is no real title available?)
• scientific article; zbMATH DE number 941396 (Why is no real title available?)
• Regular expression pattern matching for XML
• Types and programing languages

Cited in

(26)

• Type soundness for path polymorphism
• Pattern matching as cut elimination
• A typed pattern calculus
• Expression reduction systems with patterns
• Abstract canonical presentations
• Semantic foundations for generalized rewrite theories
• Rewriting calculus with(out) types
• A framework for defining logical frameworks
• Term collections in {\(\lambda\)} and {\(\rho\)}-calculi
• From functional programs to interaction nets via the rewriting calculus
• Imperative LF meta-programming
• Towards a sharing strategy for the graph rewriting calculus
• A module calculus for Pure Type Systems
• Strong normalisation in two Pure Pattern Type Systems
• First-class patterns
• A Polymorphic Type System for the Lambda-Calculus with Constructors
• scientific article; zbMATH DE number 2163051 (Why is no real title available?)
• Domain-free pure type systems
• Narrowing based inductive proof search
• Pure type systems in rewriting logic: specifying typed higher-order languages in a first-order logical framework
• Encoding type universes without using matching modulo associativity and commutativity
• Congruence types
• Expressing combinatory reduction systems derivations in the rewriting calculus
• A \(\rho\)-calculus of explicit constraint application
• Lambda calculus with patterns
• On the confluence of lambda-calculus with conditional rewriting

Describes a project that uses

Uses Software

• TREX

This page was built for publication: Pure patterns type systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2942930)