School of Computer Science
University of Nottingham
Monday, 8 June 2009, 14:00 (note the unusual weekday!)
Cybernetica Bldg (Akadeemia tee 21), room B101
Abstract: Tarski coined the name "High School Algebra" for the algebraic theory of a semiring with exponentiation. The intended interpretation are the natural numbers and Tarski conjectured that High School Algebra is complete - however this was refuted by Wilkie. DiCosmo observed that High School Algebra can also be interpreted as isomorphisms in a lambda calculus with coproducts (biCCCs) and that Wilkie's counterexample corresponds to an isomorphism which is valid in this calculus but which cannot be derived by composing isomorphisms. Inspired by this interpretation we introduce "University Algebra" moving to a dependently typed lambda calculus with Pi, Sigma, and 1, 2. We observe that Wilkie's counterexample can be derived from basic isomorphisms and discuss why we think that University Algebra is actually complete, i.e. can derive all isomorphisms between finite sets.