Brazilian type checking
- 06 May 2014
- Type theory, Talks
I just gave a talk at “Semantics of proofs and certified mathematics”. I spoke about a new proof checker Chris Stone and I are working on. The interesting feature is that it has both kinds of equality, the “paths” and the “strict” ones. It is based on a homotopy type system proposed by Vladimir Voevodsky. The slides contain talk notes and explain why it is “Brazilian”.
Download slides: brazilian-type-checking.pdf
GitHub repository: https://github.com/andrejbauer/tt
Abstract: Proof assistants verify that inputs are correct up to judgmental equality. Proofs are easier and smaller if equalities without computational content are verified by an oracle, because proof terms for these equations can be omitted. In order to keep judgmental equality decidable, though, typical proof assistants use a limited definition implemented by a fixed equivalence algorithm. While other equalities can be expressed using propositional identity types and explicit equality proofs and coercions, in some situations these create prohibitive levels of overhead in the proof.
Voevodsky has proposed a type theory with two identity types, one propositional and one judgmental. This lets us hypothesize new judgmental equalities for use during type checking, but generally renders the equational theory undecidable without help from the user.
Rather than reimpose the full overhead of term-level coercions for judgmental equality, we propose algebraic effect handlers as a general mechanism to provide local extensions to the proof assistant's algorithms. As a special case, we retain a simple form of handlers even in the final proof terms, small proof-specific hints that extend the trusted verifier in sound ways.
andrejbauer@mathstodon.xyz, I will
gladly respond.
You are also welcome to contact me directly.
Comments
Is the name some kind of sick joke? "Yeah, Brazil, some faraway place out of the way. Even there they can check our proofs." Did you know there are four mathematicians from Brazilian institutions speaking (one plenarist) at the upcoming ICM in Seoul? Maybe you should have called your program "Slovenia".
@Felipe: I have had a couple of people express a similar sentiment. I am sorry you feel this way. You are taking it completely the wrong way, of course this has nothing to do with actual Brazil.
In the live talk I explained that "Brazil" came up in discussions at the Institute for Advanced Study as just a way of speaking that "the proofs are sent somewhere far away". We needed a name for "somewhere". For some reason Brazil caught on. I do not actually know who was the first to say "Brazil" but I am pretty sure it was not me.
You see, one can always take almost anything in bad faith. For instance, I could read your comment as saying "look how Brazil is superior to Slovenia -- there are four Brazilians speaking at ICM in Seoul but no Slovenians -- Slovenia is such a backward country". Is that how you meant your comment to be read? I am sure you have not, and I am not going to read it that way. So I ask you to take our naming the system "Brazil" as homage to Brazil. Would you like me to invent reasons why it is honorable to call it Brazil? Here is one: some very close mathematician friends of mine are from Brazil. Another one: I really love the mathematically minded stories "Labyrinths" by Borges (that's a joke!). Or maybe: the system is called after the movie "Brazil", not the country. I find such post festum invention of arguments pointless. I much prefer to be honest about it: we called it Brazil for the simple reason that our conversations went smoother if we could all imagine in an anthropomorphic way an external agent who would check proofs. I have no idea why we picked Brazil. That's that.
I am happy to believe you when you say you meant no offense but the fact that I wasn't the only one to complain should indicate that it is offensive and I hope you consider changing the name. By the way, I know nothing about Slovenia and only mentioned it to give you a taste of your own medicine.
I am sure you have nothing to do with that, but the term "tropical geometry" also has its roots in a tasteless joke about Brazil, which now is too late to change.
When I read 'Brazilian type checking' I though maybe tropical semirings would be involved...
I was thinking Brazilian logic, that is paraconsistent logic. (That is actually named after mathematicians from Brasil.)