20 citations · 79 across the 14 of their papers we have counts for
Showing 2015Show all
2 papers · 1 filter
cs.LO2015
Undecidability of Equality in the Free Locally Cartesian Closed Category (Extended version)
Simon Castellan, Pierre Clairambault, Peter Dybjer
We show that a version of Martin-Löf type theory with an extensional identity type former I, a unit type N1 , Sigma-types, Pi-types, and a base type is a free category with familie…
cs.LO2015★ 9 cited
Bounding linear head reduction and visible interaction through skeletons
Pierre Clairambault
In this paper, we study the complexity of execution in higher-order programming languages. Our study has two facets: on the one hand we give an upper bound to the length of interac…