[Alta-Logic] peripatetic seminars this Friday

[Jonathan Gallagher]

There are two very special peripatetic seminars this Friday, March 3!
Details below.

The first is *Chad Nester*'s graduate seminar.

*Title:*  Turing Categories and Realizability
*Location:* ICT 616 at 12:30 pm on March 3
*Abstract:*
Realizability is an interesting way to relate computation to logic. In a
realizability model for a system of logic, a proposition is provable in
case there is a computable function witnessing this in a constructive
sense. Notions of computation have historically been defined in terms of
partial functions on sets, but need not be. Turing categories present
computation in a very general categorical framework, allowing us to study
computation more abstractly. This raises the question of how realizability
works in the more abstract setting. We approach this question through a
generalization of the category of assemblies. In addition to being of
independent interest, these generalized assemblies allow us to construct
realizability toposes more abstractly, and in the presence of less
structure than classical set-based constructions.

Second, Richard Zach has a visitor,* Matthias Baaz*,
from the Vienna University of Technology.  Matthias
has agreed to speak at a joint peripatetic-CS theory
seminar.

*Title:* Unsound inferences make proofs shorter
(joint work with Juan.P.Aguilera)
*Location: *ICT 616 at 2pm on March 3
*Abstract:*
We give examples of analytic sequent calculi that extend Gentzen's sequent
calculus LK by unsound quantifier rules in such a way that (i) derivations
lead only to true sequents and (ii) cut free proofs may be non-elementary
shorter than cut free LK proofs. This research is based on properties of
Hilbert's epsilon calculus and part of efforts to complement Hilbert's
stepwise concept of proof by useful global concepts.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.ucalgary.ca/pipermail/alta-logic-l/attachments/20170301/59460580/attachment.html