Pure type systems with definitions

DOI10.1007/3-540-58140-5_30MaRDI QIDQ4501161zbMATH OpenFDO

Authors Erik Poll, Paula Severi

Publication date 3 September 2000

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://research.tue.nl/nl/publications/bd30c197-761d-4d1b-bc72-aca434448fd4

Mathematics Subject Classification ID

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

Recommendations

• The structural theory of pure type systems
• scientific article; zbMATH DE number 2185650
• Pure type systems with explicit substitution
• A generic normalisation proof for pure type systems
• Pure type systems with explicit substitutions

Cited in

(29)

• On -conversion in the -cube and the combination with abbreviations
• Higher-order subtyping
• De Bruijn's syntax and reductional behaviour of \(\lambda\)-terms: The typed case
• Pure type systems with explicit substitution
• scientific article; zbMATH DE number 2185650 (Why is no real title available?)
• scientific article; zbMATH DE number 2185711 (Why is no real title available?)
• scientific article; zbMATH DE number 2086242 (Why is no real title available?)
• Remarks on the equational theory of non-normalizing pure type systems
• Strong normalisation in two Pure Pattern Type Systems
• Embeddability of ptykes
• A generic normalisation proof for pure type systems
• Condensing lemmas for pure type systems with universes
• Existence and uniqueness of normal forms in pure type systems with -conversion
• Pure type systems with more liberal rules
• Extensions to type systems can preserve operational equivalences
• Pure Type Systems with de Bruijn Indices
• scientific article; zbMATH DE number 2154395 (Why is no real title available?)
• Domain-free pure type systems
• Remarks on the equational theory of non-normalizing pure type systems
• Automath and Pure Type Systems
• Tactics and parameters
• ANF preserves dependent types up to extensional equality
• The structural theory of pure type systems
• Pure type systems with explicit substitutions
• An induction principle for pure type systems
• Is sized typing for Coq practical?
• A prismoid framework for languages with resources
• Pure type systems without explicit contexts
• Intersection types via finite-set declarations

This page was built for publication: Pure type systems with definitions

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