SCS
Student
Seminar
Series

go to the list of abstracts
abstracts

go to the list of previous talks
previous talks

go to the list of other SCS seminars
scs seminars

go to the SCS home page
SCS

go to the CMU home page
CMU

     

The Next Talk Fa'16 Talks General Info Speaking Req't

A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory

Monday, October 3rd, 2016 from 12-1 pm in GHC 6501.

Kuen-Bang Hou (Favonia), CSD

Following recent investigations of the use of homotopy type theory to give machine-checked proofs of constructions from homotopy theory, we constructed a mechanized proof of a result called the Blakers-Massey connectivity theorem, which relates the higher-dimensional loop structures of two spaces sharing a common part (represented by a pushout type, which is a generalization of a disjoint sum type) to those of the common part itself. This theorem gives important information about the pushout type, and has a number of useful corollaries, including the Freudenthal suspension theorem, which was used in previous formalizations. The proof is more direct than existing ones that apply in general category-theoretic settings for homotopy theory, and its mechanization is concise and high-level, due to novel combinations of ideas from homotopy theory and from type theory.

Because of the time limit, I will not show the proof of the main theorem, but will demonstrate how this theorem leads to the Freudenthal suspension theorem, an important corollary for understanding higher-dimensional loop structures of spheres.

This is joint work with Eric Finster, Eric Finster, Dan Licata and Peter LeFanu Lumsdaine, and was presented under the same title in LICS 2016.

In partial fulfillment of the Speaking Requirement.


Fall 2016 Schedule
Fri, Sep 2 GHC 4303 AVAILABLE
Fri, Sep 9 GHC 4303 AVAILABLE
Mon, Sep 12 GHC 6501 AVAILABLE
Fri, Sep 16 GHC 4303 AVAILABLE
Mon, Sep 19 GHC 6501 AVAILABLE
Fri, Sep 23 GHC 4303 AVAILABLE
Mon, Sep 26 GHC 6501 Zhou Yu Engagement in Interactive Multimodal Conversational System
Fri, Sep 30 GHC 4303 AVAILABLE
Mon, Oct 3 GHC 6501 Kuen-Bang Hou (Favonia) A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory
Fri, Oct 7 GHC 4303 AVAILABLE
Mon, Oct 10 GHC 6501 Yuzuko Nakamura Factors affecting bimanual grasping
Fri, Oct 14 GHC 4303 Mu Li MXNet: Flexible Deep Learning Framework from Distributed GPU Clouds to Embedded Systems
Mon, Oct 17 GHC 6501 AVAILABLE
Fri, Oct 21 GHC 4303 AVAILABLE
Mon, Oct 24 GHC 6501 AVAILABLE
Fri, Oct 28 GHC 4303 AVAILABLE
Mon, Oct 31 GHC 6501 AVAILABLE
Fri, Nov 4 GHC 4303 AVAILABLE
Mon, Nov 7 GHC 6501 AVAILABLE
Fri, Nov 11 GHC 4303 AVAILABLE
Mon, Nov 14 GHC 6501 AVAILABLE
Fri, Nov 18 GHC 4303 AVAILABLE
Mon, Nov 21 GHC 6501 AVAILABLE
Fri, Nov 25 GHC 4303 Thanksgiving UNAVAILABLE
Mon, Nov 28 GHC 6501 AVAILABLE
Fri, Dec 2 GHC 4303 AVAILABLE
Mon, Dec 5 GHC 6501 AVAILABLE
Fri, Dec 9 GHC 4303 AVAILABLE
Mon, Dec 12 GHC 6501 AVAILABLE


General Info

The Student Seminar Series is an informal research seminar by and for SCS graduate students from noon to 1 pm on Mondays and Fridays. Lunch is provided by the Computer Science Department (personal thanks to Sharon Burks and Debbie Cavlovich!). At each meeting, a different student speaker will give an informal, 40-minute talk about his/her research, followed by questions/suggestions/brainstorming. We try to attract people with a diverse set of interests, and encourage speakers to present at a very general, accessible level.

So why are we doing this and why take part? In the best case scenario, this will lead to some interesting cross-disciplinary work among people in different fields and people may get some new ideas about their research. In the worst case scenario, a few people will practice their public speaking and the rest get together for a free lunch.


Guideline & Speaking Requirement Need-to-Know

Note: Step #1 below are applicable to all SSS speakers. You can schedule AT MOST THREE talks per semester.

SSS is an ideal forum for SCS students to give presentations that count toward fulfilling their speaking requirements. The specifics, though, vary with each department. For instance, students in CSD will need to be familiar with the notes in Section 8 of the Ph.D. document and follow the instructions outlined on the Speakers Club homepage. Roughly speaking, these are the steps:

  1. Schedule a talk with SSS by sending your talk title, abstract, additional info (like "Joint work with..." or "In Partial Fulfillment of the Speaking Requirement"), and a picture of yourself (preferably jpeg) to sss@cs at least TWO WEEKS before your scheduled talk.
  2. After you are confirmed with your SSS slot, go to the Speakers Club Calendar and schedule your talk at least THREE WEEKS in advance of the talk date.
  3. On the day of your talk, make sure you print Speakers Club evaluation forms for your evaluators to use.
Students outside of CSD will need to check with their respective departments regarding the procedure. As another example, ISRI students fulfill their speaking requirements by attending a semesterly Software Research Seminar and giving X number of presentations per school year. If you have experience with your department that might help others in your department, please feel free to contribute your knowledge by emailing us. Thank you!


SSS Coordinators

Armaghan Naik, Computational Biology
Lin Xiao, CSD

 


Web contact: sss+www@cs