Would there be interest in an Agda introduction?

Showing 1-44 of 44 messages
Would there be interest in an Agda introduction? Cactus 6/4/12 4:24 AM
Hi FPers o' Singapore,

So when Don was doing his talk last time at the meetup, there was some
interest in Agda and dependent type systems, and I may or may not have
said that I would be willing to do a talk. So, my question is, how real
is that interest?

I just realized that I could probably do one based on the
MIU proof I posted yesterday (https://gist.github.com/2863448): you
wouldn't necessarily become an Agda expert (hell, I'm definitely not one
yet...) but I could hopefully explain enough so that that example code
would make sense afterwards.

Or, depending (heh) on the audience's interest, I could do one aimed at
elementary algebra by preparing something based on my modular arithmetic
stuff.

Bye,
         Gergo

--

   .--= ULLA! =-----------------.
    \     http://gergo.erdi.hu   \
     `---= ge...@erdi.hu =-------'
How can I insert disk #3 when only two will fit?
Re: Would there be interest in an Agda introduction? Kenny Zhuo Ming Lu 6/4/12 4:28 AM
I am definitely interested in it.

Kenny
Re: Would there be interest in an Agda introduction? Maxim Moiseev 6/4/12 4:35 AM
+1

Max

Re: Would there be interest in an Agda introduction? Kerneltrap 6/4/12 4:51 AM
Count me in.

Andrew
Re: Would there be interest in an Agda introduction? zan 6/4/12 6:35 AM
it would be good to have a meetup this month. we have a lot of new members to the mailing list recently. are there any suitable offices available for a meetup?
Re: Would there be interest in an Agda introduction? Kenny Zhuo Ming Lu 6/4/12 6:49 AM
I can try to book a room in the school if you guys don't mind coming to NYP which is near Yio Chu Kang.
Re: Would there be interest in an Agda introduction? Mike Mazur 6/4/12 7:21 AM
Hi,

On Mon, Jun 4, 2012 at 9:49 PM, Lu Zhuo Ming <luzh...@gmail.com> wrote:
> I can try to book a room in the school if you guys don't mind coming to NYP
> which is near Yio Chu Kang.

I'm pretty sure New Context can host, same venue as Don's talk. Just
let me know the dates and I'll double confirm.

Mike
Re: Would there be interest in an Agda introduction? zan 6/7/12 3:49 PM
may i suggest 27 june for the meetup? feel free to suggest an alternative date if you cannot make it.
Re: Would there be interest in an Agda introduction? Raymond Tay 6/7/12 6:33 PM
+1 i like to come--
http://about.me/rayt
Re: Would there be interest in an Agda introduction? Kenny Zhuo Ming Lu 6/7/12 6:39 PM
+1 
Re: Would there be interest in an Agda introduction? Kerneltrap 6/7/12 7:23 PM
Would it be possible to make it earlier? Around 20 june?

On Fri, Jun 8, 2012 at 6:49 AM, zan <lian...@gmail.com> wrote:

Re: Would there be interest in an Agda introduction? Chien 6/7/12 7:56 PM
Come on, either 20 or 27 would be fine!
Re: Would there be interest in an Agda introduction? zan 6/7/12 8:08 PM
i'm ok with 20th. i suggested 27 to give the presenters more time to prepare. so the tentative date is 20th? is {new context} office available?
Re: Would there be interest in an Agda introduction? Mike Mazur 6/7/12 8:16 PM
Hi,

The 20th or 27th are currently available. I can only secure the space for sure once the date is confirmed. 

Mike
Re: Would there be interest in an Agda introduction? Cactus 6/7/12 8:34 PM

I'd prefer 27 so that I have more time to prepare. On the 26th, of course.

Re: Would there be interest in an Agda introduction? Kenny Zhuo Ming Lu 6/7/12 9:07 PM
Let's stick to 27 then? 

Regards,
Kenny
Re: Would there be interest in an Agda introduction? Maysam 6/7/12 10:35 PM
20 June +1

Re: Would there be interest in an Agda introduction? Shaun Martin 6/7/12 10:40 PM
+1
-- I can make it on 27th, but not on 20th.
Re: Would there be interest in an Agda introduction? Mike Mazur 6/8/12 12:29 AM
Hi,

Alright, the New Context office is booked for June 27. What time are we starting?

Mike
Re: Would there be interest in an Agda introduction? Raymond Tay 6/8/12 1:26 AM
Hey Mike,

I've never been to the next context office. can you provide me/us the address again? 

Re: Would there be interest in an Agda introduction? Kenny Zhuo Ming Lu 6/8/12 8:17 AM
7:30pm?
Re: Would there be interest in an Agda introduction? Kerneltrap 6/8/12 8:33 AM
8:15pm?
Re: Would there be interest in an Agda introduction? zan 6/8/12 7:14 PM
i think 8.15pm is too late. it will cause the meetup to end very late. 7.30pm looks good.
Re: Would there be interest in an Agda introduction? Mike Mazur 6/9/12 1:06 AM
Hi,

New Context is at 53A Craig Road in Tanjong Pagar, above the wine
shop. The entrance is on the side of the building, right next to the
soccer court.

7:30pm also sounds like a late start to me :-) but that's no problem.

Mike
Re: Would there be interest in an Agda introduction? Cactus 6/11/12 6:44 PM

So, I just realized that 27th is a Wednesday. Can we move it to Thursday or preferably Friday?

Re: Would there be interest in an Agda introduction? TH Lim 6/11/12 10:51 PM
Friday would be good, we can hang out longer. However, if it is on Wed, I try to make it.

On Tue, Jun 12, 2012 at 9:44 AM, Dr. ÉRDI Gergő <ge...@erdi.hu> wrote:

So, I just realized that 27th is a Wednesday. Can we move it to Thursday or preferably Friday?

On Jun 9, 2012 4:07 PM, "Mike Mazur" <mma...@gmail.com> wrote:
Hi,

New Context is at 53A Craig Road in Tanjong Pagar, above the wine
shop. The entrance is on the side of the building, right next to the
soccer court.

7:30pm also sounds like a late start to me :-) but that's no problem.

Mike


On Sat, Jun 9, 2012 at 10:14 AM, zan <lian...@gmail.com> wrote:
> i think 8.15pm is too late. it will cause the meetup to end very late.
> 7.30pm looks good.
>
>
> On Friday, June 8, 2012 11:33:30 PM UTC+8, Kerneltrap wrote:
>>
>> 8:15pm?
>>
>> On Fri, Jun 8, 2012 at 11:17 PM, Lu Zhuo Ming <luzh...@gmail.com> wrote:
>>>
>>> 7:30pm?
>>>
>>>
>>> On Fri, Jun 8, 2012 at 3:29 PM, Mike Mazur <mma...@gmail.com> wrote:
>>>>
>>>> Hi,
>>>>
>>>> Alright, the New Context office is booked for June 27. What time are we
>>>> starting?
>>>>
>>>> Mike
>>>>
>>>>
>>>>
>>>>
>>>> On 8 Jun, 2012, at 12:07, Lu Zhuo Ming <luzh...@gmail.com> wrote:
>>>>
>>>> Let's stick to 27 then?
>>>>
>>>> Regards,
>>>> Kenny
>>>>
>>>> On Fri, Jun 8, 2012 at 11:34 AM, Dr. ÉRDI Gergő <ge...@erdi.hu> wrote:
>>>>>
>>>>> I'd prefer 27 so that I have more time to prepare. On the 26th, of
>>>>> course.
>>>>>
>>>>> On Jun 8, 2012 11:16 AM, "Mike Mazur" <mma...@gmail.com> wrote:
>>>>>>
>>>>>> Hi,
>>>>>>
>>>>>> The 20th or 27th are currently available. I can only secure the space
>>>>>> for sure once the date is confirmed.
>>>>>>
>>>>>> Mike
>>>>>>
>>>>>>
>>>>>>
>>>>>> On 8 Jun, 2012, at 11:08, zan <lian...@gmail.com> wrote:
>>>>>>
>>>>>> i'm ok with 20th. i suggested 27 to give the presenters more time to
>>>>>> prepare. so the tentative date is 20th? is {new context} office available?
>>>>>>
>>>>>> On Friday, June 8, 2012 10:56:32 AM UTC+8, Chien wrote:
>>>>>>>
>>>>>>> Come on, either 20 or 27 would be fine!
>>>>>>>
>>>>>>>
>>>>>>> On Fri, Jun 8, 2012 at 10:23 AM, let rec <shwe...@gmail.com> wrote:
>>>>>>>>
>>>>>>>> Would it be possible to make it earlier? Around 20 june?
>>>>>>>>
>>>>>>>> On Fri, Jun 8, 2012 at 6:49 AM, zan <lian...@gmail.com> wrote:
>>>>>>>>>
>>>>>>>>> may i suggest 27 june for the meetup? feel free to suggest an
>>>>>>>>> alternative date if you cannot make it.
>>>>>>>>>
>>>>>>>>>
>>>>>>>>> On Monday, June 4, 2012 10:21:17 PM UTC+8, Mike Mazur wrote:
>>>>>>>>>>
>>>>>>>>>> Hi,
>>>>>>>>>>
>>>>>>>>>> On Mon, Jun 4, 2012 at 9:49 PM, Lu Zhuo Ming <luzh...@gmail.com>
>>>>>>>>>> wrote:
>>>>>>>>>> > I can try to book a room in the school if you guys don't mind
>>>>>>>>>> > coming to NYP
>>>>>>>>>> > which is near Yio Chu Kang.
>>>>>>>>>>
>>>>>>>>>> I'm pretty sure New Context can host, same venue as Don's talk.
>>>>>>>>>> Just
>>>>>>>>>> let me know the dates and I'll double confirm.
>>>>>>>>>>
>>>>>>>>>> Mike
>>>>>>>>
>>>>>>>>
>>>>>>>
>>>>
>>>
>>
>

Re: Would there be interest in an Agda introduction? Mike Mazur 6/11/12 11:10 PM
Hi,

I can't make it on Friday. You'd have to find another space. 

Sorry!
Mike
Re: Would there be interest in an Agda introduction? zan 6/11/12 11:30 PM
is {new context} available on thursday?
Re: Would there be interest in an Agda introduction? Mike Mazur 6/12/12 12:10 AM
Hi,

Thursday should be fine. 

Mike
Re: Would there be interest in an Agda introduction? Cactus 6/20/12 12:55 AM

So just to confirm, it's 28th Thursday, 7 pm?

I have my slides ready btw, just some slight finishing touches needed.

G

Re: Would there be interest in an Agda introduction? Mike Mazur 6/20/12 6:18 AM
Hi,

On Wed, Jun 20, 2012 at 3:55 PM, Dr. ÉRDI Gergő <ge...@erdi.hu> wrote:
> So just to confirm, it's 28th Thursday, 7 pm?
>
> I have my slides ready btw, just some slight finishing touches needed.

The space is still booked for Wednesday, June 27. Thursday still looks
available. Should I change the booking?

Thanks,
Mike
Re: Would there be interest in an Agda introduction? Cactus 6/20/12 6:20 AM
On Wed, 20 Jun 2012, Mike Mazur wrote:

> The space is still booked for Wednesday, June 27. Thursday still looks
> available. Should I change the booking?

Yes please.

--

   .--= ULLA! =-----------------.
    \     http://gergo.erdi.hu   \
     `---= ge...@erdi.hu =-------'
Nyomd meg egyszer az ESC-et a kilépéshez és kétszer az elmentéshez
Re: Would there be interest in an Agda introduction? Cactus 6/24/12 6:27 PM

Hi,

So can I get a confirmation on the 28th date?

Thanks,
Gergo

Re: Would there be interest in an Agda introduction? Mike Mazur 6/24/12 8:37 PM
Hi,

On 25 Jun, 2012, at 9:27, "Dr. ÉRDI Gergő" <ge...@erdi.hu> wrote:

So can I get a confirmation on the 28th date?

Sorry, I forgot to email you. Last week I changed the booking to Thursday, the 28th, so the space is secured.

Hopefully everyone else has updated their calendars and doesn't show up on Wednesday :-)

Thanks,
Mike

Re: Would there be interest in an Agda introduction? Kenny Zhuo Ming Lu 6/25/12 4:31 AM
To sum up.

Venue: 53A Craig Road Singapore 089691
Time: 28 July 2012 7:30pm

Speaker: Gergo,
Title: Introduction to Agda

See you all there!

Cheers,
Kenny
Re: Would there be interest in an Agda introduction? Raymond Tay 6/25/12 4:53 AM
28 June instead of July or was there a change in date?
Re: Would there be interest in an Agda introduction? Cactus 6/25/12 4:54 AM

June. This Thursday.

Re: Would there be interest in an Agda introduction? Chien 6/25/12 6:19 AM
Thanks.
Re: Would there be interest in an Agda introduction? Kenny Zhuo Ming Lu 6/28/12 8:47 AM
I would like to thank Gergő for the wonderful talk tonight. The topic covered a wide range of interesting points, including Curry Howard isomorphism, GADT, theorem prover, finiteness and countability, termination, etc. 

I guess most of us are not quite satisfied with the hasty ending of the talk due the time constraint, let's quickly have a continued talk next month. 

I would also like to thank Mike and crews from the New Context for the warm hospitality. 

@Gergő if you don't mind, could you share us the slides?

For interesting talk like this, we might think about taping it and share it on some public channel. 

Regards,
Kenny
Re: Would there be interest in an Agda introduction? Mike Mazur 6/28/12 4:29 PM
Hi,

On Thu, Jun 28, 2012 at 11:47 PM, Lu Zhuo Ming <luzh...@gmail.com> wrote:
> I would like to thank Gergő for the wonderful talk tonight. The topic
> covered a wide range of interesting points, including Curry Howard
> isomorphism, GADT, theorem prover, finiteness and countability, termination,
> etc.

Yes, thanks Gergő for putting the presentation together.

> I guess most of us are not quite satisfied with the hasty ending of the talk
> due the time constraint, let's quickly have a continued talk next month.

Let's nail down a date for part 2 of the talk. How about Wednesday, July 25?

Thanks,
Mike
Re: Would there be interest in an Agda introduction? Kenny Zhuo Ming Lu 6/28/12 4:57 PM
July 25 is good for me. :)
Re: Would there be interest in an Agda introduction? Cactus 7/1/12 3:50 AM
On Fri, 29 Jun 2012, Mike Mazur wrote:

> On Thu, Jun 28, 2012 at 11:47 PM, Lu Zhuo Ming <luzh...@gmail.com> wrote:
>> I would like to thank Gergő for the wonderful talk tonight. The topic
>> covered a wide range of interesting points, including Curry Howard
>> isomorphism, GADT, theorem prover, finiteness and countability, termination,
>> etc.
>
> Yes, thanks Gergő for putting the presentation together.

Actually (as I'm sure you could tell) I had a blast as well:)

>> I guess most of us are not quite satisfied with the hasty ending of the talk
>> due the time constraint, let's quickly have a continued talk next month.
>
> Let's nail down a date for part 2 of the talk. How about Wednesday, July 25?

I'm never available on Wednesdays. Otherwise -- I'll have to check my
schedule tomorrow about that week.

I've uploaded the slides (source & PDF; includes all the slides I skipped
or didn't have time to) to http://gergo.erdi.hu/projects/agda/sg-meetup/.

As for part 2, it seemed (based on questions I got at the venue and also
since then in private correspondence) that equality was a tricky topic, so
I think I'll whip up some more slides on equality (and equivalence
relations in general). Anything else that was particularily unclear?

Bye,
         Gergo


--

   .--= ULLA! =-----------------.
    \     http://gergo.erdi.hu   \
     `---= ge...@erdi.hu =-------'
Egér: az elefánt japán változata
Re: Would there be interest in an Agda introduction? Mike Mazur 7/1/12 5:40 AM
Hi,

On Sun, Jul 1, 2012 at 6:50 PM, Dr. ERDI Gergo <ge...@erdi.hu> wrote:
> On Fri, 29 Jun 2012, Mike Mazur wrote:
>> On Thu, Jun 28, 2012 at 11:47 PM, Lu Zhuo Ming <luzh...@gmail.com> wrote:
>>> I guess most of us are not quite satisfied with the hasty ending of the
>>> talk
>>> due the time constraint, let's quickly have a continued talk next month.
>>
>> Let's nail down a date for part 2 of the talk. How about Wednesday, July
>> 25?
>
> I'm never available on Wednesdays. Otherwise -- I'll have to check my
> schedule tomorrow about that week.

Sounds good. Let's pencil in Thursday, July 26 then, pending your confirmation.

Thanks,
Mike
Re: Would there be interest in an Agda introduction? Cactus 7/2/12 6:24 PM

Ok so I just checked, 26th looks doable.

More topics »