Type-checking injective pure type systems

DOI10.1017/S0956796899003573zbMATH Open0949.03027WikidataQ114116617 ScholiaQ114116617MaRDI QIDQ4948007FDOQ4948007

Authors: Gilles Barthe 

Publication date: 6 December 2000

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

Recommendations

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

zbMATH Keywords

lambda calculustype-checking algorithmexpansion postponementinjective pure type systemstyped sorts

Mathematics Subject Classification ID

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

Cited In (6)

• Checking Emptiness of Non-Deterministic Regular Types with Set Operators
• An induction principle for pure type systems
• Domain-free pure type systems
• A partial type checking algorithm for Type:Type
• Interfacing Coq + SSReflect with GAP
• Programming Languages and 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)