Epilogue

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.

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).

This entry was posted on Tuesday, January 10th, 2006 at 11:09 am and is filed under General. You can follow any responses to this entry through the RSS 2.0 feed. You can skip to the end and leave a response. Pinging is currently not allowed.