research
∙
05/11/2023
Layered Modal Type Theories
We introduce layers to modal type theories, which subsequently enables t...
share
research
∙
11/22/2022
A Categorical Normalization Proof for the Modal Lambda-Calculus
We investigate a simply typed modal λ-calculus, λ^→□, due to Pfenning, W...
research
∙
06/15/2022
An Investigation of Kripke-style Modal Type Theories
This technical report investigates Kripke-style modal type theories, bot...
research
∙
06/06/2022
A Category Theoretic View of Contextual Types: from Simple Types to Dependent Types
We describe the categorical semantics for a simply typed variant and a s...
research
∙
03/02/2021
Internal Category with Families in Presheaves
In this note, we review a construction of category with families (CwF) i...
research
∙
05/14/2020