17 citations · 38 across the 8 of their papers we have counts for
11 papers
Sundance: A Simple SMT Solver for Program Verification
Amar Shah, Benjamin F. Jones, Can Cebeci +6
We present Sundance, an SMT solver for program verification written in about 13,600 lines of Rust. Sundance combines the Cadical SAT solver with congruence closure, linear arithmet…
Normalization by Evaluation with Substitutions as Operations
Jason Z. S. Hu
In previous works on normalization by evaluation (NbE) with an untyped domain model, explicit substitutions are a major decision choice, which, in retrospect, is taken to simplify…
Contravariant Universe Subtyping, Formalized, Mechanized
Shengyi Jiang, Jason Z. S. Hu
In a type theory with a cumulative universe hierarchy, \emph{subtyping} is often incorporated to lift lower universe levels to higher ones. In practice, kernels of proof assistants…
DeLaM: A Dependent Layered Modal Type Theory for Meta-programming
Jason Z. S. Hu, Brigitte Pientka
We scale layered modal type theory to dependent types, introducing DeLaM, dependent layered modal type theory. This type theory is novel in that we have one uniform type theory in…
Layered Modal Type Theories
Jason Z. S. Hu, Brigitte Pientka
We introduce layers to modal type theories, which subsequently enables type theories for pattern matching on code in meta-programming and clean and straightforward semantics.
A Categorical Normalization Proof for the Modal Lambda-Calculus
Jason Z. S. Hu, Brigitte Pientka
We investigate a simply typed modal -calculus, , due to Pfenning, Wong and Davies, where we define a well-typed term with respect to a context stack that capture…
A Category Theoretic View of Contextual Types: from Simple Types to Dependent Types
Jason Z. S. Hu, Brigitte Pientka, Ulrich Schöpp
We describe the categorical semantics for a simply typed variant and a simplified dependently typed variant of Cocon, a contextual modal type theory where the box modality mediates…
An Investigation of Kripke-style Modal Type Theories
Jason Z. S. Hu, Brigitte Pientka
This technical report investigates Kripke-style modal type theories, both simply typed and dependently typed. We examine basic meta-theories of the type theories, develop their sub…
Internal Category with Families in Presheaves
Jason Z. S. Hu
In this note, we review a construction of category with families (CwF) in a presheaf category. When the base category of a presheaf category is a CwF, we internalize this CwF struc…
Formalizing of Category Theory in Agda
Jason Z. S. Hu, Jacques Carette
The generality and pervasiness of category theory in modern mathematics makes it a frequent and useful target of formalization. It is however quite challenging to formalize, for a…
Undecidability of and Its Decidable Fragments
Jason Hu, Ondřej Lhoták
Dependent Object Types (DOT) is a calculus with path dependent types, intersection types, and object self-references, which serves as the core calculus of Scala 3. Although the cal…