Type Theory Study Group

Contact owners and managers

1–30 of 48

Welcome to our type theory study group. We're an online group interested in talking about types and their applications to logic, mathematics, and computer science.

This group is a beginner-friendly place to learn type theory, but we're just getting started. If it looks more like a construction site than an onramp right now, stay tuned! We'll get started in a month or so.

Next meeting: Saturday, Dec 12 at 16:30 EST, 21:30 GMT

Material: Ch 3 and 4 of PFPL

Hosts: Mark Farrell and Danny Gratzer

0 selected

David Smith, Steven Shaw2

8/28/19

That's great, thanks. I'll join noobs. I never did finish TTFP.

unread,

That's great, thanks. I'll join noobs. I never did finish TTFP.

8/28/19

Matt Oliveri, … Hendrik Boom7

8/3/16

Possible topic for focused study and discussion

Whoa, I missed these messages from ~2 months after my original post. Now I reply ~1/2 month late. :\

unread,

Possible topic for focused study and discussion

Whoa, I missed these messages from ~2 months after my original post. Now I reply ~1/2 month late. :\

8/3/16

Mark Farrell, … Gershom B15

4/24/16

A Revised Proposal for the Objective and Agenda of the Study Group

As an observer to this list who hasn't participated, but who has some experience and advice to

unread,

A Revised Proposal for the Objective and Agenda of the Study Group

As an observer to this list who hasn't participated, but who has some experience and advice to

4/24/16

Hendrik Boom, Matt Oliveri2

4/22/16

alternative foundations of mathamatics

AFAICT, the main disagreement between Harvey Friedman and the HoTT proponents is simply over what

unread,

alternative foundations of mathamatics

AFAICT, the main disagreement between Harvey Friedman and the HoTT proponents is simply over what

4/22/16

Matt Oliveri, Cyrus Omar3

1/31/16

Coinductive Big-Step Semantics

(Here is a non-paywall copy: ftp://ftp.disi.unige.it/person/AnconaD/Ancona-FTfJP14.pdf) I see. So it

unread,

Coinductive Big-Step Semantics

(Here is a non-paywall copy: ftp://ftp.disi.unige.it/person/AnconaD/Ancona-FTfJP14.pdf) I see. So it

1/31/16

Ilan Godik, Hendrik Boom4

1/31/16

Meeting 4: 30.01.2016

The recording of the meeting is avaliable here: https://www.youtube.com/watch?v=_JfAyMe5uLA Cheers,

unread,

Meeting 4: 30.01.2016

The recording of the meeting is avaliable here: https://www.youtube.com/watch?v=_JfAyMe5uLA Cheers,

1/31/16

Craig Stuntz, … Jimmy Burrell5

1/20/16

Why learn type theory?

Well done, Joseph. Succinct and to the point. On Sunday, November 1, 2015 at 2:25:16 PM UTC-6, Joseph

unread,

Why learn type theory?

Well done, Joseph. Succinct and to the point. On Sunday, November 1, 2015 at 2:25:16 PM UTC-6, Joseph

1/20/16

1/14/16

Organization of Meeting #4: Dynamics and Type Safety

Hello everyone. The topics for the next meeting are: Chapter 5: Dynamics Chapter 6: Type Safety - I

unread,

Organization of Meeting #4: Dynamics and Type Safety

Hello everyone. The topics for the next meeting are: Chapter 5: Dynamics Chapter 6: Type Safety - I

1/14/16

Craig Stuntz, Matt Oliveri2

1/12/16

contextual / structural dynamics vs operational semantics?

Contextual and structural dynamics are two (closely related) styles of operational semantics. Other

unread,

contextual / structural dynamics vs operational semantics?

Contextual and structural dynamics are two (closely related) styles of operational semantics. Other

1/12/16

Mark Farrell, … Ilan Godik11

1/9/16

Meeting #4: Dynamics and Type Safety?

You are definitely welcome. There are many in this group like you, coming with one background or

unread,

Meeting #4: Dynamics and Type Safety?

You are definitely welcome. There are many in this group like you, coming with one background or

1/9/16

1/8/16

Re: [Type Theory] Digest for type-theory-study-group@googlegroups.com - 5 updates in 1 topic

I'm looking forward to resuming! For what it's worth, I can make Sunday, but not Saturday (at

unread,

Re: [Type Theory] Digest for type-theory-study-group@googlegroups.com - 5 updates in 1 topic

I'm looking forward to resuming! For what it's worth, I can make Sunday, but not Saturday (at

1/8/16

Mark Farrell, Alex Moore - Niemi3

1/5/16

Introduction to Higher Type Theory - Daniel Licata's PhD Thesis

this is quite interesting to me so far -- thanks for the share On Saturday, December 12, 2015 at 3:41

unread,

Introduction to Higher Type Theory - Daniel Licata's PhD Thesis

this is quite interesting to me so far -- thanks for the share On Saturday, December 12, 2015 at 3:41

1/5/16

Alex Moore - Niemi, … Matt Oliveri38

12/25/15

Immediately above, it was explained that a state that can't take a step is called "stuck

unread,

Immediately above, it was explained that a state that can't take a step is called "stuck

12/25/15

Gary Fixler, Joseph Abrahamson2

12/18/15

Is type theory not a mathematical theory?

Type Theory could be said to be related to a few on that list... But much more accurate is to say

unread,

Is type theory not a mathematical theory?

Type Theory could be said to be related to a few on that list... But much more accurate is to say

12/18/15

Craig Stuntz, … Ilan Godik3

12/16/15

Interesting tool: Shared PDF annotations

If stability is a problem, we can use it via IPFS (addressed by the content's hash), which makes

unread,

Interesting tool: Shared PDF annotations

If stability is a problem, we can use it via IPFS (addressed by the content's hash), which makes

12/16/15

Joseph Abrahamson, Mark Farrell3

12/13/15

Discussion group

I feel like the more material generated the better! There are people at all different levels on this

unread,

Discussion group

I feel like the more material generated the better! There are people at all different levels on this

12/13/15

Mark Farrell, Joseph Abrahamson2

12/12/15

Discussion Leader Interest Survey

This is great! Thanks for putting this together! On Sat, Dec 12, 2015 at 3:23 PM Mark Farrell <

unread,

Discussion Leader Interest Survey

This is great! Thanks for putting this together! On Sat, Dec 12, 2015 at 3:23 PM Mark Farrell <

12/12/15

Danny Gratzer, Mark Farrell5

12/12/15

Are you able to send out an invite to the hangout? On Friday, December 11, 2015 at 9:41:40 AM UTC-5,

unread,

Are you able to send out an invite to the hangout? On Friday, December 11, 2015 at 9:41:40 AM UTC-5,

12/12/15

Mark Farrell, … Cyrus Omar17

12/8/15

Meeting #3: Chapter 3 of PFPL?

Added a rough overview, agenda and some supplementary readings to the Hackpad. Thoughts? On Tuesday,

unread,

Meeting #3: Chapter 3 of PFPL?

Added a rough overview, agenda and some supplementary readings to the Hackpad. Thoughts? On Tuesday,

12/8/15

Gary Fixler, Mark Farrell4

12/4/15

Benjamin C. Pierce books?

Sorry, code: MITGIFTS, and it's still working atm. On Friday, December 4, 2015 at 1:55:47 PM UTC-

unread,

Benjamin C. Pierce books?

Sorry, code: MITGIFTS, and it's still working atm. On Friday, December 4, 2015 at 1:55:47 PM UTC-

12/4/15

Mark Farrell, … Craig Stuntz4

12/4/15

Paper of the Week?

Having a list of papers/books/lectures on the syllabus as optional reading would make a lot of sense,

unread,

Paper of the Week?

Having a list of papers/books/lectures on the syllabus as optional reading would make a lot of sense,

12/4/15

Mark Farrell, Aggelos Biboudis3

12/4/15

Conferences and Events

Excellent - thank you! On Friday, December 4, 2015 at 8:56:22 AM UTC-5, Aggelos Biboudis wrote: Last

unread,

Conferences and Events

Excellent - thank you! On Friday, December 4, 2015 at 8:56:22 AM UTC-5, Aggelos Biboudis wrote: Last

12/4/15

12/4/15

Proposed Future Topics

Hi all, I've (also) been trying to compile a list of "proposed future topics" detailing

unread,

Proposed Future Topics

Hi all, I've (also) been trying to compile a list of "proposed future topics" detailing

12/4/15

12/3/15

I created a barebones syllabus a few weeks back as a place to draft plans for future meetings +

unread,

I created a barebones syllabus a few weeks back as a place to draft plans for future meetings +

12/3/15

Joseph Abrahamson, … Jonathan Sterling8

11/28/15

Hackpad, Hangout, and Invite for Tomorrow's Meeting

Joseph, Could you send me and Darin an invite to the hangout please? Darin may show up, but no

unread,

Hackpad, Hangout, and Invite for Tomorrow's Meeting

Joseph, Could you send me and Darin an invite to the hangout please? Darin may show up, but no

11/28/15

Joseph Abrahamson, … Jonathan Sterling12

11/27/15

NEW: Special Topics Meeting with Jon Sterling

Hi everyone, I think barring any issues we should go ahead with tomorrow at 9:30 PM GMT. I will put

unread,

NEW: Special Topics Meeting with Jon Sterling

Hi everyone, I think barring any issues we should go ahead with tomorrow at 9:30 PM GMT. I will put

11/27/15

Irene Knapp, … Suhail Shergill5

11/18/15

Timezone survey results

We should figure out if there's anything else we want to ask; I'll happily run another survey

unread,

Timezone survey results

We should figure out if there's anything else we want to ask; I'll happily run another survey

11/18/15

Joseph Abrahamson, … Steven Shaw5

11/14/15

Huh, never would have thought of ABTs as a logical framework. Something to ponder on. On 14 November

unread,

Huh, never would have thought of ABTs as a logical framework. Something to ponder on. On 14 November

11/14/15

Ilan Godik, Mark Farrell2

11/14/15

Thanks Ilan. On Friday, November 13, 2015 at 7:32:05 PM UTC-5, Ilan Godik wrote: Hello everyone. I

unread,

Thanks Ilan. On Friday, November 13, 2015 at 7:32:05 PM UTC-5, Ilan Godik wrote: Hello everyone. I

11/14/15

Shon Feder, … Joseph Abrahamson11

11/13/15

Local, irl, Auxilliary Meetings?

Yeah, I've thought about crossposting to that group, but at the moment I'd rather reach out

unread,

Local, irl, Auxilliary Meetings?

Yeah, I've thought about crossposting to that group, but at the moment I'd rather reach out

11/13/15

Search

Clear search

Close search

Google apps

Main menu