scientific article; zbMATH DE number 4120168

zbMath0684.03025MaRDI QIDQ4733863

Thomas Streicher

Publication date: 1988

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

polymorphic lambda calculuscalculus of constructionsterm modelcontextual categoriescalculi of dependent types

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Abstract data types; algebraic specification (68Q65) Categorical logic, topoi (03G30) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Theories (e.g., algebraic theories), structure, and semantics (18C10) Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50) Combinatory logic and lambda calculus (03B40)

Related Items (10)

A higher-order calculus and theory abstraction ⋮ On explicit substitutions and names (extended abstract) ⋮ Independence results for calculi of dependent types ⋮ Dictoses ⋮ Proving strong normalization of CC by modifying realizability semantics ⋮ Alpha conversion, conditions on variables and categorical logic ⋮ Inheritance as implicit coercion ⋮ Comprehension categories and the semantics of type dependency ⋮ Unnamed Item ⋮ Proof-search in type-theoretic languages: An introduction

This page was built for publication: