research
∙
05/11/2023
Layered Modal Type Theories
We introduce layers to modal type theories, which subsequently enables t...
share
research
∙
04/29/2023
Can ChatGPT Pass An Introductory Level Functional Language Programming Course?
The recent introduction of ChatGPT has drawn significant attention from ...
research
∙
01/06/2023
Identifying Different Student Clusters in Functional Programming Assignments: From Quick Learners to Struggling Students
Instructors and students alike are often focused on the grade in program...
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
∙
10/07/2022
Novice Type Error Diagnosis with Natural Language Models
Strong static type systems help programmers eliminate many errors withou...
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
∙
11/15/2021
Moebius: Metaprogramming using Contextual Types – The stage where System F can pattern match on itself (Long Version)
We describe the foundation of the metaprogramming language, Moebius, whi...
research
∙
05/07/2019
A Type Theory for Defining Logics and Proofs
We describe a Martin-Löf-style dependent type theory, called Cocon, that...
research
∙
01/10/2019
Cocon: Computation in Contextual Type Theory
We describe a Martin-Löf style dependent type theory, called Cocon, that...
research
∙
05/01/2018