13 citations · 23 across the 7 of their papers we have counts for
4 papers · 1 filter
Reflections on existential types
Jonathan Sterling
Existential types are reconstructed in terms of small reflective subuniverses and dependent sums. The folklore decomposition detailed here gives rise to a particularly simple accou…
Sheaf semantics of termination-insensitive noninterference
Jonathan Sterling, Robert Harper
We propose a new sheaf semantics for secure information flow over a space of abstract behaviors, based on synthetic domain theory: security classes are open/closed partitions, type…
A cost-aware logical framework
Yue Niu, Jonathan Sterling, Harrison Grodin +1
We present , a ost-ware ogical ramework for studying quantitative aspects of functional programs. Taking inspiration…
Nominal LCF: A Language for Generic Proof
Jonathan Sterling
The syntax and semantics of user-supplied hypothesis names in tactic languages is a thorny problem, because the binding structure of a proof is a function of the goal at which a ta…