Objects and subtyping in the --calculus modulo

DOI10.4230/LIPICS.TYPES.2014.47MaRDI QIDQ5277971zbMATH OpenFDO

Authors Raphaël Cauderlier, Catherine Dubois

Publication date 12 July 2017

Full work available at URL https://doi.org/10.4230/LIPICS.TYPES.2014.47

zbMATH Keywords

dependent typeencodinglambda-Pi-calculusobject calculusrewrite system

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18) Grammars and rewriting systems (68Q42) Semantics in the theory of computing (68Q55)

Recommendations

• Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo
• scientific article; zbMATH DE number 6744143
• Publication:4934325
• An interpretation of typed objects into typed -calculus
• An imperative object calculus

Cited in

(3)

• An interpretation of typed objects into typed -calculus
• ML pattern-matching, recursion, and rewriting: from FoCaLiZe to Dedukti
• Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo

Describes a project that uses

Uses Software

• dedukti

This page was built for publication: Objects and subtyping in the \(\lambda\)-\(\Pi\)-calculus modulo

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