28 citations · 116 across the 28 of their papers we have counts for
Showing 2018Show all
3 papers · 1 filter
cs.LO2018★ 1 cited
Normalization by gluing for free λ-theories
Jonathan Sterling, Bas Spitters
The connection between normalization by evaluation, logical predicates and semantic gluing constructions is a matter of folklore, worked out in varying degrees within the literatur…
cs.LO2018★ 5 cited
The RedPRL Proof Assistant (Invited Paper)
Carlo Angiuli, Evan Cavallo, Kuen-Bang Hou +2
RedPRL is an experimental proof assistant based on Cartesian cubical computational type theory, a new type theory for higher-dimensional constructions inspired by homotopy type the…
cs.LO2018★ 6 cited
Guarded Computational Type Theory
Jonathan Sterling, Robert Harper
Nakano's later modality can be used to specify and define recursive functions which are causal or synchronous; in concert with a notion of clock variable, it is possible to also ca…