Normalization by evaluation for modal dependent type theory
From MaRDI portal
Publication:6065506
DOI10.1017/s0956796823000060OpenAlexW4387270836MaRDI QIDQ6065506
Jason Z. S. Hu, Brigitte Pientka, Junyoung Jang
Publication date: 11 December 2023
Published in: Journal of Functional Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1017/s0956796823000060
Cites Work
- Definitional interpreters for higher-order programming languages
- MetaML and multi-stage programming with explicit annotations
- On an intuitionistic modal logic
- Fitch-style modal lambda calculi
- A functional correspondence between call-by-need evaluators and lazy abstract machines
- A judgmental reconstruction of modal logic
- Intuitionistic model constructions and normalization proofs
- Type Theory Should Eat Itself
- Type theory in type theory using quotient inductive types
- Tagless staged interpreters for typed languages
- Programming and Reasoning with Guarded Recursion for Coinductive Types
- A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
- A modal analysis of staged computation
- Inductive-Inductive Definitions
- A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family
- Extensional Rewriting with Sums
- A general formulation of simultaneous inductive-recursive definitions in type theory
- Brouwer's fixed-point theorem in real-cohesive homotopy type theory
- Internal type theory
- Categorical reconstruction of a reduction free normalization proof
- Multimodal Dependent Type Theory
- Modal dependent type theory and dependent right adjoints
- On equivalence and canonical forms in the LF type theory
- Normalisation by Evaluation for Dependent Types.
- Semantical Analysis of Modal Logic I Normal Modal Propositional Calculi
- Primitive recursion for higher-order abstract syntax
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
