Meeting #3: Chapter 3 of PFPL?

[Mark Farrell]

Hi all,

(Special thanks to Jon Sterling, Darin Morrison and Joseph for leading the "special topics" meeting on abstract binding trees tonight.)

- Should we start thinking about the next meeting now?
- Will we move on to chapter 3 of PFPL?

(Is talking about hypothetical judgments a good time to start alluding to their appearance in constructive proposition logic and moving on to simple type theory / scoping with lambda abstractions?)

-Mark

[Craig Stuntz]

It doesn't really feel like we've talked about chapter 2, or the homework, yet? Are people feeling done with 1+2 for now, or would it be best to have another discussion with different hosts to focus on chapter 2?

[Danny Gratzer]

I think it would be best to move on to chapter 3. Perhaps the discussion will be 30 minutes new material

and 30 minutes example problems. However these first few chapters are really hard to motivate without

pressing on a bit; a lot of this material will fall into place as we keep going.

If we talk about chapter 3 this time then the meeting after that we can actually dive into understanding

programming languages :)

Cheers,

Danny

[Joseph Abrahamson]

I'm very much with Danny on this one. We've spent about a month on Ch 1 and 2. At this point we probably *could* go through it thoroughly, but it'd be more fun to get to real material. At this point, people who encounter issues later will have Ch 1 and 2 and all of the notes as resources to patch up misunderstandings.

So I'm in favor of moving on to Ch 3.

[Aggelos Biboudis]

+1 for moving on to Ch 3.

(hi all btw, Aggelos from Greece and I am applauding this initiative)

--
You received this message because you are subscribed to the Google Groups "Type Theory Study Group" group.
To unsubscribe from this group and stop receiving emails from it, send an email to type-theory-study...@googlegroups.com.
To post to this group, send email to type-theory...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/type-theory-study-group/a6400e8e-0dbc-4ab1-8bc1-b2b3d85073ae%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--

 Aggelos.

[Jon Sterling]

Yes, moving to Ch 3 sounds like a good idea. I think people have
probably had their fill of syntax—and probably many will not fully
understand what went down in Ch 1-2 anyway until they have seen some of
the concrete examples which come later in the book.

best,
jon

> > <https://groups.google.com/d/msgid/type-theory-study-group/a6400e8e-0dbc-4ab1-8bc1-b2b3d85073ae%40googlegroups.com?utm_medium=email&utm_source=footer>
> > .

> > For more options, visit https://groups.google.com/d/optout.
> >
> --
> Aggelos.
>

> --
> You received this message because you are subscribed to the Google Groups
> "Type Theory Study Group" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to type-theory-study...@googlegroups.com.
> To post to this group, send email to
> type-theory...@googlegroups.com.
> To view this discussion on the web visit

> https://groups.google.com/d/msgid/type-theory-study-group/CAHLSyCmg0v6i__Ars7m%2BpSAuvX1Ov-GZUrf2YX8W%2BoFWVsx79Q%40mail.gmail.com.

[Cyrus Omar]

I'd suggest covering Chapters 3 and 4 simultaneously. Chapter 4 makes the material in Chapter 3 a bit more concrete (and should probably be read/covered first).

To view this discussion on the web visit https://groups.google.com/d/msgid/type-theory-study-group/1448989295.2556200.454875081.63C185C7%40webmail.messagingengine.com.

[Jon Sterling]

Yes, I'd forgotten that Ch. 3 is still part of the logical framework
stuff. I don't think that students need to feel like they "really"
understand all of Ch. 3 before making progress elsewhere, so combining
it with Ch. 4 (which provides a number of examples of actually using the
framework that Ch. 3 propounds) is a good idea, I think. Getting to some
concrete examples seems really important; otherwise, I think the
exercise of understanding bob's logical framework without having used it
will be just too frustrating.

-- jon

> > https://groups.google.com/d/msgid/type-theory-study-group/1448989295.2556200.454875081.63C185C7%40webmail.messagingengine.com

[Joseph Abrahamson]

I think that’s a good idea. We can get to an actual type system before the holidays :)

—

Joseph Abrahamson

@tel / sdbo / jspha.com

To view this discussion on the web visit https://groups.google.com/d/msgid/type-theory-study-group/1448993708.2573127.454949585.1B5EAFCF%40webmail.messagingengine.com.

[Mark Farrell]

Decide on a date soon? Maybe next Saturday at 4:30 PM EST?

On Saturday, November 28, 2015 at 6:20:21 PM UTC-5, Mark Farrell wrote:

[Danny Gratzer]

Saturday December 12th (8 days away) seems like a good date to me.

We still have not had anyone volunteer to lead this one and this group will be a bit more fun

if it's not just Craig, Joseph, and me talking. If no one else does volunteer than I can help

lead this one.

Cheers,

Danny Gratzer

[Mark Farrell]

I'd like to finish chapters 3 and 4 first before agreeing to volunteer, but am interested; I hope/intend to do the work this weekend.

[Craig Stuntz]

Cyrus, would you be willing to be a host for a meeting sometime? Doesn't have to be the next one, but would appreciate your expertise!

Also, it might make sense to reach out to some people outside this group with expertise in type systems, like Robert Harper (obviously!), Stephanie Weirich, Benjamin C. Pierce, etc.?

On Friday, December 4, 2015 at 8:59:05 AM UTC-5, Danny Gratzer wrote:

[Cyrus Omar]

Sure, I'd be happy to lead one soon, but I can't lead this next one.

[Mark Farrell]

Somebody want to create a HackPad for the proposed upcoming meeting? Might be useful for planning purposes.

[Mark Farrell]

Ah, here we go: https://ttsg.hackpad.com/Type-Theory-Study-Group-Meeting-3-Smo7poCD2ql

[Mark Farrell]

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