28 citations · 116 across the 28 of their papers we have counts for
Showing 2016Show all
3 papers · 1 filter
math.LO2016★ 3 cited
Higher-Order Functions and Brouwer's Thesis
Jonathan Sterling
Extending Martín Escardó's effectful forcing technique, we give a new proof of a well-known result: Brouwer's monotone bar theorem holds for any bar that can be realized by a funct…
cs.PL2016
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…
cs.LO2016
Syntax and Semantics of Abstract Binding Trees
Jonathan Sterling, Darin Morrison
The contribution of this paper is the development of the syntax and semantics of multi-sorted nominal abstract binding trees (abts), an extension of second order universal algebra…