3 citations · 5 across the 4 of their papers we have counts for
5 papers
Natural Deduction Derivations as Directed Acyclic Proof Graphs
Jonathan Chan, Aaron Stump
In conventional natural deduction, a proof of a proposition is a derivation tree constructed out of inference rules with some number of premises and a conclusion judgement. For pro…
Internalizing Extensions in Lattices of Type Theories
Jonathan Chan
Many proof assistants allow the use of features and axioms that increase their expressive power. However, these extensions must be used with care, as some combinations are known to…
Bounded First-Class Universe Levels in Dependent Type Theory
Jonathan Chan, Stephanie Weirich
In dependent type theory, being able to refer to a type universe as a term itself increases its expressive power, but requires mechanisms in place to prevent Girard's paradox from…
Stratified Type Theory
Jonathan Chan, Stephanie Weirich
A hierarchy of type universes is a rudimentary ingredient in the type theories of many proof assistants to prevent the logical inconsistency resulting from combining dependent func…
Is Sized Typing for Coq Practical?
Jonathan Chan, Yufeng Li, William J. Bowman
Contemporary proof assistants such as Coq require that recursive functions be terminating and corecursive functions be productive to maintain logical consistency of their type theo…