Conversation

Jacques Carette
@jjcarett2
Beautiful new preprint arxiv.org/abs/2104.09366 showing how to do Schemes in Isabelle. To me, the most interesting thing is a rediscovery that if you have a complex enough interface language (here: locales) you can overcome a weak object language (here: HOL).
arxiv.org
Simple Type Theory is not too Simple: Grothendieck's Schemes...
Church's simple type theory is often deemed too simple for elaborate mathematical constructions. In particular, doubts were raised whether schemes could be formalized in this setting and a...
1
18
Jacques Carette
@jjcarett2
Why rediscovery? Because Goguen et al. had already seen this with Clear/OBJ: you can do all the higher-order stuff you need with a first-order object language if you have a higher-order "module" language at your disposal.
3
3
Larry Diehl
@larrytheliquid
another interesting recent take is 1ML's for first-class modules. even if the distinctions are too rigid you can combine levels but with appropriate predicativity (or analogous mechanism) restrictions
1
1
Jacques Carette
@jjcarett2
Yes, 1ML is very nice. It takes its design environment (ML, strong phase distinction, no dependent types) very seriously, and arrives at a pleasant conclusion. I want something as elegant as that, but for a dependently typed system. Very different design environment.
1
3
Jacques Carette
@jjcarett2
Various things collapse to be 'the same' in the presence of dependent types. Arend, for example, takes real advantage of that. There's a lot of research waiting to be done in that space.
2
5