Typing in pure type systems

DOI10.1006/inco.1993.1038zbMath0785.03003OpenAlexW2120300141MaRDI QIDQ1260645

L. S. van Benthem Jutting

Publication date: 30 August 1993

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1006/inco.1993.1038

zbMATH Keywords

typed lambda calculifunctional structurefunctional systemsdecidability of typing relationgeneralized type systemsnon-functional systemsuniqueness of domains

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Combinatory logic and lambda calculus (03B40)

Related Items (8)

Unified Syntax with Iso-types ⋮ The expansion postponement in pure type systems ⋮ Checking algorithms for Pure Type Systems ⋮ Closure under alpha-conversion ⋮ Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence ⋮ Implicit coercions in type systems ⋮ Cut Elimination in a Class of Sequent Calculi for Pure Type Systems ⋮ Type inference for pure type systems

This page was built for publication: Typing in pure type systems