37 citations · 133 across the 20 of their papers we have counts for
Showing 2017Show all
3 papers · 1 filter
cs.LO2017
Computational Higher Type Theory III: Univalent Universes and Exact Equality
Carlo Angiuli, Kuen-Bang Hou, Robert Harper
This is the third in a series of papers extending Martin-Löf's meaning explanations of dependent type theory to a Cartesian cubical realizability framework that accounts for higher…
cs.LO2017★ 5 cited
Algebraic Foundations of Proof Refinement
Jonathan Sterling, Robert Harper
We contribute a general apparatus for dependent tactic-based proof refinement in the LCF tradition, in which the statements of subgoals may express a dependency on the proofs of ot…
cs.PL2017★ 2 cited
A Higher-Order Logic for Concurrent Termination-Preserving Refinement
Joseph Tassarotti, Ralf Jung, Robert Harper
Compiler correctness proofs for higher-order concurrent languages are difficult: they involve establishing a termination-preserving refinement between a concurrent high-level sourc…