Beyond PrimitiveAgda

[Jan Malakhovski]

Hello.

As far as I can see everyone is busy with exams.
Shall we have a meeting this Thursday?
I have nothing to tell, i.e. I didn't do anything after finishing
untyped lambda.

Concerning frequently asked question "What to do after PrimitiveAgda?".
I think the best way is to read containers' and memberships' definitions from
https://bitbucket.org/robsimmons/agda-lib/src
and to prove all the properties without peeping.

Then implement any nonempty subset of the following.
* Define an ordered container (e.g. sorted binary tree, 2-3-tree, etc)
and prove its invariants (e.g. that insert and delete preserve
sorting).
* Formalize Hilbert-style propositional calculus, Natural deduction
and (the usual rules) of Sequent calculus
(from http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.17.7385)
and prove that they prove exactly the same formulas.
* Do the same for first-order logic.
* Postulate double negation elimination (or Peirce's law) and other
nice classical things about numbers and prove something classical
about convergence (e.g. something like Riemann series theorem).

BR,
Jan

[Jan Malakhovski]

Well, looks like no TTFV today. Brake till the end of June?

[Alexey Sergushichev]

I suppose so.

---
Best regards,
Alexey Sergushichev

> --
> You received this message because you are subscribed to the Google Groups "Type Theory for Vegetables" group.
> To post to this group, send email to type-theory-f...@googlegroups.com.
> To unsubscribe from this group, send email to type-theory-for-veg...@googlegroups.com.
> For more options, visit this group at http://groups.google.com/group/type-theory-for-vegetables?hl=en.
>