NEW: Special Topics Meeting with Jon Sterling

[Joseph Abrahamson]

Hi everyone,

During the first TTSG meeting Craig mentioned that Jon Sterling would have an interesting perspective on the current topic of study—ABTs and judgements over them—as he's the implementer of a number of very nice ABT libraries in various languages. 

More than that, it turns out that he's recently been focusing some of his research effort into understanding extensions to and refinements of the sorts of ABTs we approach in PFPL, so he'll be able to talk about the subject ranging from the basics of implementation all the way to cutting edge theory.

I spoke with him offline and mentioned running a Special Topics meeting for TTSG on "Implementing and Extending PFPL's ABTs" to pick his brain on these topics and he agreed! So let's talk about details!

- This meeting is extracurricular to PFPL. The material will begin by connecting to what we've studied so far but may extend past that and in novel directions. If this is your first time digging into Type Theory, we'll spend lots of time trying to answer questions both on and offline, but be prepared for short excursions into the deep end. If you're more of a Type Theory veteran, then help by asking questions which really deepen the material we're studying and connect it to Jon's work and experience.

- This meeting will be a Hangouts on Air again with notes in Hackpad and corresponding live chat on Freenode's ##typetheory channel.

- Alongside Jon we'd like to have a "co-host/panelist" to ask questions and support some conversation. By default, I'm more than happy to do this, but I think that Danny would also be able to do a great job here given his work with Jon on JonPRL. It'd be great to have more nominees and volunteers as well (I think Darin Morrison would also be a good co-panelist here).

- We need to pick a time and date. Based on Irene's survey times like 4:30 PM EST work well across the whole group making it an after-lunch meeting for Jon. I therefore propose we try to have the meeting on Saturday the 28th at 4:30 PM EST, but we can discuss that, too.

- I propose that the meeting is 1 hour+ where we try to have everyone online for at least one hour and, should enough interest remain as gauged by the Hackpad and by members in IRC, we can extend it so long as the panelists have time.

Anyway, this initial planning aside I'd like to hear from you, members of TTSG, what works best, what topics interest you the most, and how to make this meeting a success.

And Jon, please feel free to take the floor and talk about what topics you'd be most interested in discussing given the context.

Cheers,

Joseph

[David Christiansen]

Hi all,

I haven't had a lot of participation yet (this is my first email to the
list!) but I think this sounds like a great idea. I agree that Darin
would be a good panel member, as well as Danny.

16:30 US Eastern time is quite late for those of use in Central European
time, as that's 22:30, but I don't mind staying up a bit for an exciting
topic!

/David

On 20/11/15 18:01, Joseph Abrahamson wrote:
> Hi everyone,
>
> During the first TTSG meeting Craig mentioned that Jon Sterling would have
> an interesting perspective on the current topic of study—ABTs and
> judgements over them—as he's the implementer of a number of very nice ABT
> libraries in various languages.
>
> More than that, it turns out that he's recently been focusing some of his
> research effort into understanding extensions to and refinements of the
> sorts of ABTs we approach in PFPL, so he'll be able to talk about the
> subject ranging from the basics of implementation all the way to cutting
> edge theory.
>
>
>

> I spoke with him offline and mentioned running a *Special Topics meeting
> for TTSG on "Implementing and Extending PFPL's ABTs"* to pick his brain on

> these topics and he agreed! So let's talk about details!
>

> - This meeting is *extracurricular* to PFPL. The material will begin by

> connecting to what we've studied so far but may extend past that and in
> novel directions. If this is your first time digging into Type Theory,
> we'll spend lots of time trying to answer questions both on and offline,
> but be prepared for short excursions into the deep end. If you're more of a
> Type Theory veteran, then help by asking questions which really deepen the
> material we're studying and connect it to Jon's work and experience.
>
> - This meeting will be a Hangouts on Air again with notes in Hackpad and
> corresponding live chat on Freenode's ##typetheory channel.
>
> - Alongside Jon we'd like to have a "co-host/panelist" to ask questions and

> support some conversation. *By default*, I'm more than happy to do this,
> but I think that *Danny* would also be able to do a great job here given
> his work with Jon on JonPRL. It'd be great to have more *nominees and
> volunteers* as well (I think *Darin Morrison* would also be a good
> co-panelist here).
>
> - *We need to pick a time and date.* Based on Irene's survey times like

> 4:30 PM EST work well across the whole group making it an after-lunch

> meeting for Jon. I therefore propose we try to have the meeting on *Saturday
> the 28th* at *4:30 PM EST*, but we can discuss that, too.
>
> - I propose that the meeting is *1 hour+ *where we try to have everyone

> online for at least one hour and, should enough interest remain as gauged
> by the Hackpad and by members in IRC, we can extend it so long as the
> panelists have time.
>
>
>

> Anyway, this initial planning aside I'd like to hear from *you*, members of

[Joseph Abrahamson]

22:30 *is* late. :(

If we moved it to West Coast mornings that might work but it'd be very tough for AUS of where we seem to have a few members from data from Irene's survey. There's not really any great answers to coordinating such a distributed meeting.

(P.S. It'd be great having you do a "special topics" meeting, too, David. I was really sad that I missed seeing you talk on Idris in DC a few years ago. :)

[Adam Sandberg Eriksson]

I haven't had a lot of conversation before as well. (I'd prefer meetings during weekends or later at night (announced not to too late!!)

Cheers from Sweden!

Adam Sandberg Ericsson



Adam Sandberg Ericsson

> --
> 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/564F548C.5010104%40davidchristiansen.dk.
> For more options, visit https://groups.google.com/d/optout.

[Ilan Godik]

At least the chosen time is an improvement from last time, when it was in the early hours of the night in European time.

Cheers,

Ilan Godik.

On 20/11/15 18:01, Joseph Abrahamson wrote: 

[David Christiansen]

On 20/11/15 19:11, Joseph Abrahamson wrote:
> (P.S. It'd be great having you do a "special topics" meeting, too, David. I
> was really sad that I missed seeing you talk on Idris in DC a few years
> ago. :)

It was recorded!

In any case, I'd be happy to do this. Let's set it up after the current
one has run successfully.

/David

[Miles Sabin]

On Fri, Nov 20, 2015 at 5:12 PM, David Christiansen
<da...@davidchristiansen.dk> wrote:
> 16:30 US Eastern time is quite late for those of use in Central European
> time, as that's 22:30, but I don't mind staying up a bit for an exciting
> topic!

Seconded ... it's never going to be possible to find a single time
which will please everyone, but this pretty much guarantees you won't
see any Europeans.

Could we try two/three times evenly spaced around the clock and rotate
between them? That plus regular recordings would help a lot.

Cheers,


Miles

--
Miles Sabin
tel: +44 7813 944 528
skype: milessabin
gtalk: mi...@milessabin.com
http://milessabin.com/blog
http://twitter.com/milessabin

[Joseph Abrahamson]

Yeah, the survey seemed to suggest that most of the European members of the group were in UTC or UTC+1, so this compromise landed here.

What would be better, I think, is to do as you suggest and try to get a few meetings together at various times. This wouldn't be possible (I don't think) for a meeting like this one centered around a special topic or opportunity, but the general meetings could be organized that way. I'd love to hear about anyone interested in running such a meeting!

[Mark Farrell]

Meeting tomorrow?

[Danny Gratzer]

That is the plan! Sadly I'm not going to be able to make this one.. I'll be traveling all of tomorrow.  
However I definitely support Darrin cohosting and Joseph could also go on and make sure the discussion hits all the points raised on irc and written down? If this is recorded than I can also watch and post my notes.

Sorry about the late notice, things only became clear today :/

--

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/2726fc3d-da60-4f1a-8c59-3647c11c5130%40googlegroups.com.

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

--

Cheers,

Danny Gratzer

[Jonathan Sterling]

Hi All,

Can someone remind me exactly what time this is supposed to be? (I think saw 22:30 GMT in the thread, but I wanted to make sure I didn't read the wrong thing). Assuming this is scheduled during my waking hours on the West Coast of the US, I'll be available to answer any questions anyone has on ABTs. (Sadly, though, I'm on vacation away from home and will not have access to my blackboard, which would have made things a lot easier! What I need is a document camera, heh.)

As for Darin, nobody from here actually asked him if he was willing to come on and talk, so I wouldn't take it as a given that he'll be available; I might have mentioned it to him a few days ago, but let's play it by ear. I'll catch up with him again and find out if he wants to do it. In any case, I hope that by suggesting that Darin would have very interesting things to say, I did not give anyone the impression that he had in fact agreed to do it.

Is there a document of collected questions or areas of confusion on ABTs that I can look at? I was planning to discuss the indexed families operators in more depth, and explain the semantics of symbolic parameters, unless there is something more pressing; the other thing that there seemed to be a lot of confusion about was the relationship between the "sorts" in an ABT signature, and the types of a programming language (which might use ABTs as its uniform syntax), so I planned also to clarify this.

Best,

Jon

To unsubscribe from this group and stop receiving emails from it, send an email to type-theory-study-group+unsub...@googlegroups.com.
To post to this group, send email to type-theory-study-group@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/type-theory-study-group/2726fc3d-da60-4f1a-8c59-3647c11c5130%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--

Cheers,

Danny Gratzer

[Joseph Abrahamson]

Hi everyone,

I think barring any issues we should go ahead with tomorrow at 9:30 PM GMT. I will put together a Hackpad for questions and announce it in a short bit.

I dropped the ball slightly in between some work and holiday items, otherwise I would have made more formal preparations for it. I am still planning on being available at this time and, if it works for Jon, then I can organize and provide some questions.

To anyone listening live, I'll also be in Freenode ##typetheory and be tracking new question on the Hackpad.

Jon, if you'd like to reach out to Darin that'd be great—or I'd be happy to otherwise. Since it's late notice let us not hold any expectation that he'll be able to make it, however. I hope I didn't early in just suggesting he might be able to provide interesting context for these topics as well.