61 citations · 90 across the 12 of their papers we have counts for
Showing 2014Show all
3 papers · 1 filter
cs.LO2014★ 3 cited
An Introduction to the Clocked Lambda Calculus
Jörg Endrullis, Dimitri Hendriks, Jan Willem Klop +1
We give a brief introduction to the clocked lambda calculus, an extension of the classical lambda calculus with a unary symbol tau used to witness the beta-steps. In contrast to th…
cs.LO2014
Extensionality of lambda-*
Andrew Polonsky
We prove an extensionality theorem for the "type-in-type" dependent type theory with Sigma-types. We suggest that the extensional equality type be identified with the logical equiv…
cs.LO2014★ 1 cited
Internalization of extensional equality
Andrew Polonsky
We give a type system in which the universe of types is closed by reflection into it of the logical relation defined externally by induction on the structure of types. This contrib…