It’s a surprise, I know, but with any luck we might be about to manage a workblip in between all the anonymous refereeing, workshop attendance, workshop organisation, paper polishing, RAE-bashing and running out of money. I know, I know, don’t speak too soon. But a peculiar astrological pattern has brought Nicolas, Morris and myself into an unprecedented degree of availability, even as it takes us to three different countries, so you might spot some darcs activity.
Nicolas is in the business of splitting * into Prop and Set. Prop is closed under False, True, ∧, ∀, =, and later we’ll add coinductive relations. It’s a Tarski-style universe with an explicit Prf : Prop → Set, so it’s straightforward to identify all inhabitants of Prf P definitionally. Pleasingly, the observational equality on propositions expands (P : Prop) = (Q : Prop) as (P => Q) ∧ (Q => P), where P => Q is short for ∀x:Prf P. Q. Trans-European comedy with quotient sets will follow shortly.
Meanwhile, Peter and I are getting back to working on the representation of the proof state. Morally, the proof state is a flat sequence of longnamed fully λ-lifted definitions in various states of repair. The trick, however, is to scrunch this sequence into a tree to improve sharing (of parameters and of name prefixes) and to reflect the hierarchical structure of development. Reports of updates get propagated from global to local; requests for updates get propagated from local to global. It’s life in a dissection, scheduling threads. The amusing thing is the way this process fits a with distributed computing model, whether we want it to or not.