[Colloquium] REMINDER: Research at TTIC: David McAllester, TTIC

[Dawn Ellis]

When:     Friday, October 24th at noon

Where:    TTIC, 6045 S Kenwood Avenue, 5th Floor, Room 526

Who:       David McAllester, TTIC

Title:       Morphoid Type Theory

Abstract:

This talk will present a type-theoretic foundation for
mathematics in which each type is associated with an equivalence
relation in correspondence with the standard notions of isomorphism in
mathematics.  The main result is an abstraction theorem stating that
isomorphic objects, such as isomorphic graphs or homeomorphic topological
spaces,
are inter-substitutable in well-typed contexts.
The talk will also present ``Voldemort's theorem'' which states that a
non-canonical object cannot be named by a well-type expression.  For
example, no well-typed expression can name an isomorphism between a
general finite dimensional vector space and its dual.

The type expressions of this system can be assigned a simple semantics
in which each type expression denotes a set. However, the general
definition of isomorphism and the abstraction theorem both rely on a
sophisticated semantics in which each type denotes a ``morphoid'' ---
a generalization of the concept of groupoid (a groupoid is a category in
which each morphism is an isomorphism).  Closed type expressions (type
expressions without free variables) denote groupoids (a special case
of morphoids).  A variable declaration x:tau declares x to be an
isomorphism in the morphoid tau.  Of particular interest is the
variable declaration alpha:type which declares alpha to be an
isomorphism in the groupoid of types.  But this also declares alpha to
itself be a type and hence a morphoid.  Each morphoid plays two roles
--- it specifies the set of isomorphisms that are instances of the
morphoid and, at the same time, is itself a type isomorphism.  Hence
the term ``morphoid''.



***************************************
Research at TTIC Seminar Series

TTIC is hosting a weekly seminar series presenting the research currently
underway at the Institute. Every week a different TTIC faculty member will
present their research.  The lectures are intended both for students
seeking research topics and adviser, and for the general TTIC and
University of Chicago communities interested in hearing what their
colleagues are up to.

To receive announcements about the seminar series, please subscribe to the
mailing list: https://groups.google.com/a/ttic.edu/group/talks/subscribe

Speaker details can be found at: http://www.ttic.edu/tticseminar.php.

For additional questions, please contact David McAllester at
mcallester at ttic.edu


-- 
*Dawn Ellis*
Administrative Coordinator,
Bookkeeper
773-834-1757
dellis at ttic.edu

TTIC
6045 S. Kenwood Ave.
Chicago, IL. 60637
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.cs.uchicago.edu/pipermail/colloquium/attachments/20141023/8e5af051/attachment.htm