Type-checking injective pure type systems

DOI10.1017/S0956796899003573MaRDI QIDQ4948007zbMATH OpenWikidataFDO

Authors Gilles Barthe

Publication date 6 December 2000

Published in Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/S0956796899003573

zbMATH Keywords

expansion postponementinjective pure type systemslambda calculustype-checking algorithmtyped sorts

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Functional programming and lambda calculus (68N18)

Recommendations

• Type inference for pure type systems
• Typing in pure type systems

Cited in

(6)

• Domain-free pure type systems
• A partial type checking algorithm for Type:Type
• Interfacing Coq + SSReflect with GAP
• Programming Languages and Systems
• Checking Emptiness of Non-Deterministic Regular Types with Set Operators
• An induction principle for pure type systems

This page was built for publication: Type-checking injective pure type systems

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