First meeting of the year

1. UI. Some interest from Nick Thomas. Joel is planning an experiment with gtk2hs.
2. Using darcs is working very well. Discussed structure our darcs repos.
3. Status of Epigram 2. We have been hacking the core recently. The afore mentioned ‘Up’ and ‘Down’ terms are in with the supporting parser, (not very) pretty printer,type checker equality checker. Peter has been implementing datatypes. Next is the equality type, and then on to wrapping it in a representation of holes.
4. Thorsten discussed injectivity of type constructors.
5. Move to the board to discuss 3 further. Specifically Conor proposes a short path to making something go. Two main areas: a) Finishing Core and moving on to theorem prover. b) Concrete syntax, comms protocol.
DSC00017.JPG
6. Division of work. Joel and Wouter to look at concrete syntax and comms. James and Peter to look at core and theorem proving.
7. The advantages of supporting observational type theory sooner rather than later will afford us simplifications in the implementation. (Thorsten to go into more detail about this on the blog).

2 Responses to “First meeting of the year”

  1. Nick Thomas Says:

    Regarding UI: As I mentioned to Paul Callaghan, I’m pretty busy for the next few weeks, so I won’t have much time for projects on the side. So, don’t expect results from me too soon.

  2. pwm Says:

    oops, new blog software kept your comment back for moderation and I failed to spot it, you should be able to leave further comments without delay

Leave a Reply