Semantical analysis of contextual types

DOI10.1007/978-3-030-45231-5_26MaRDI QIDQ2200843zbMATH OpenOpenAlexFDO

Authors Brigitte Pientka, Ulrich Schöpp

Publication date 23 September 2020

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-45231-5_26

Mathematics Subject Classification ID

Theory of software (68Nxx) Theory of computing (68Qxx)

Recommendations

• A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types
• Contextual modal type theory
• Contextual modal type theory with polymorphic contexts
• A type theory for defining logics and proofs
• Contextual types, explained. Invited tutorial

Cites work

• scientific article; zbMATH DE number 1241699 (Why is no real title available?)
• scientific article; zbMATH DE number 512773 (Why is no real title available?)
• scientific article; zbMATH DE number 1754648 (Why is no real title available?)
• scientific article; zbMATH DE number 226803 (Why is no real title available?)
• A framework for defining logics
• A modal analysis of staged computation
• A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
• Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
• Brouwer's fixed-point theorem in real-cohesive homotopy type theory
• Comprehension categories and the semantics of type dependency
• Contextual modal type theory
• Generalized algebraic theories and contextual categories
• Inductive beluga: programming proofs
• Internal type theory
• Internal universes in models of homotopy type theory
• Well-founded recursion over contextual objects

Cited in

(3)

• A generic usage analysis with subeffect qualifiers
• Aspectual Shifts With and Without Type Conflict
• A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types

This page was built for publication: Semantical analysis of contextual types

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