Multi-level contextual type theory

DOI10.4204/EPTCS.71.3MaRDI QIDQ6940445zbMATH OpenFDO

Authors Mathieu Boespflug, Brigitte Pientka

Publication date 19 August 2025

Copyright license Creative Commons license

Full work available at URL https://doi.org/10.4204/EPTCS.71.3

Mathematics Subject Classification ID

Logic in computer science (03B70) Type theory (03B38)

Cites work

• scientific article; zbMATH DE number 1948185 (Why is no real title available?)
• A calculus of lambda calculus contexts
• 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)
• Computer Science Logic
• Contextual modal type theory
• Explicit substitutions for contextual type theory
• Hierarchical nominal terms and their theory of rewriting
• Higher-order dynamic pattern unification for dependent types and records
• Multilanguage hierarchical logics, or: How we can do without modal logics
• Optimizing higher-order pattern unification.
• The lambda-context calculus (extended version)
• Theorem proving modulo
• Typed lambda calculi and applications. 8th international conference, TLCA 2007, Paris, France, June 26--28, 2007. Proceedings.
• VeriML: typed computation of logical terms inside a language with effects

This page was built for publication: Multi-level contextual type theory

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