scientific article; zbMATH DE number 4120168
calculi of dependent typescalculus of constructionscontextual categoriespolymorphic lambda calculusterm model
Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Combinatory logic and lambda calculus (03B40) Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50) Categorical logic, topoi (03G30) Theories (e.g., algebraic theories), structure, and semantics (18C10) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Abstract data types; algebraic specification (68Q65)
- Dependence and independence results for (impredicative) calculi of dependent types
- Revisiting the categorical interpretation of dependent type theory
- Independence results for calculi of dependent types
- scientific article; zbMATH DE number 1241699
- Categorical semantics for higher order polymorphic lambda calculus
- Inheritance as implicit coercion
- Comprehension categories and the semantics of type dependency
- Proof-search in type-theoretic languages: An introduction
- Revisiting the categorical interpretation of dependent type theory
- A higher-order calculus and theory abstraction
- Products of families of types and (Pi,lambda)-structures on C-systems
- scientific article; zbMATH DE number 6694121 (Why is no real title available?)
- scientific article; zbMATH DE number 2185676 (Why is no real title available?)
- scientific article; zbMATH DE number 445156 (Why is no real title available?)
- scientific article; zbMATH DE number 4177054 (Why is no real title available?)
- Dependence and independence results for (impredicative) calculi of dependent types
- scientific article; zbMATH DE number 1241699 (Why is no real title available?)
- On explicit substitutions and names (extended abstract)
- Independence results for calculi of dependent types
- Dictoses
- CATEGORICAL MODEL CONSTRUCTION FOR PROVING SYNTACTIC PROPERTIES
- scientific article; zbMATH DE number 4187810 (Why is no real title available?)
- Proving strong normalization of CC by modifying realizability semantics
- Comprehension and quotient structures in the language of 2-categories
- From proof-theoretic validity to base-extension semantics for intuitionistic propositional logic
- Alpha conversion, conditions on variables and categorical logic
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4733863)
