Would there be interest in an Agda introduction?

103 views
Skip to first unread message

Dr. ERDI Gergo

unread,
Jun 4, 2012, 7:24:25 AM6/4/12
to singapore-functi...@googlegroups.com
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?

Lu Zhuo Ming

unread,
Jun 4, 2012, 7:28:52 AM6/4/12
to singapore-functi...@googlegroups.com
I am definitely interested in it.

Kenny

Maxim Moiseev

unread,
Jun 4, 2012, 7:35:35 AM6/4/12
to singapore-functi...@googlegroups.com
+1

Max

let rec

unread,
Jun 4, 2012, 7:51:30 AM6/4/12
to singapore-functi...@googlegroups.com
Count me in.

Andrew

zan

unread,
Jun 4, 2012, 9:35:44 AM6/4/12
to singapore-functi...@googlegroups.com
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?

Lu Zhuo Ming

unread,
Jun 4, 2012, 9:49:10 AM6/4/12
to singapore-functi...@googlegroups.com
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.

Mike Mazur

unread,
Jun 4, 2012, 10:21:17 AM6/4/12
to singapore-functi...@googlegroups.com
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

zan

unread,
Jun 7, 2012, 6:49:38 PM6/7/12
to singapore-functi...@googlegroups.com
may i suggest 27 june for the meetup? feel free to suggest an alternative date if you cannot make it.

Raymond Tay

unread,
Jun 7, 2012, 9:33:18 PM6/7/12
to singapore-functi...@googlegroups.com
+1 i like to come
--
http://about.me/rayt

Lu Zhuo Ming

unread,
Jun 7, 2012, 9:39:44 PM6/7/12
to singapore-functi...@googlegroups.com
+1 

let rec

unread,
Jun 7, 2012, 10:23:58 PM6/7/12
to singapore-functi...@googlegroups.com
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:

Chien Nguyen

unread,
Jun 7, 2012, 10:56:32 PM6/7/12
to singapore-functi...@googlegroups.com
Come on, either 20 or 27 would be fine!

zan

unread,
Jun 7, 2012, 11:08:55 PM6/7/12
to singapore-functi...@googlegroups.com
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?

Mike Mazur

unread,
Jun 7, 2012, 11:16:05 PM6/7/12
to singapore-functi...@googlegroups.com
Hi,

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

Mike

Dr. ÉRDI Gergő

unread,
Jun 7, 2012, 11:34:25 PM6/7/12
to singapore-functi...@googlegroups.com

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

Lu Zhuo Ming

unread,
Jun 8, 2012, 12:07:46 AM6/8/12
to singapore-functi...@googlegroups.com
Let's stick to 27 then? 

Regards,
Kenny

Maysam

unread,
Jun 8, 2012, 1:35:51 AM6/8/12
to singapore-functi...@googlegroups.com
20 June +1

Shaun Martin

unread,
Jun 8, 2012, 1:40:54 AM6/8/12
to singapore-functi...@googlegroups.com, singapore-functi...@googlegroups.com
+1
-- I can make it on 27th, but not on 20th.

Mike Mazur

unread,
Jun 8, 2012, 3:29:49 AM6/8/12
to singapore-functi...@googlegroups.com
Hi,

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

Mike

Raymond Tay

unread,
Jun 8, 2012, 4:26:10 AM6/8/12
to singapore-functi...@googlegroups.com
Hey Mike,

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

thanks !

Lu Zhuo Ming

unread,
Jun 8, 2012, 11:17:15 AM6/8/12
to singapore-functi...@googlegroups.com
7:30pm?

let rec

unread,
Jun 8, 2012, 11:33:30 AM6/8/12
to singapore-functi...@googlegroups.com
8:15pm?

zan

unread,
Jun 8, 2012, 10:14:50 PM6/8/12
to singapore-functi...@googlegroups.com
i think 8.15pm is too late. it will cause the meetup to end very late. 7.30pm looks good.

Mike Mazur

unread,
Jun 9, 2012, 4:06:33 AM6/9/12
to singapore-functi...@googlegroups.com
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

Dr. ÉRDI Gergő

unread,
Jun 11, 2012, 9:44:32 PM6/11/12
to singapore-functi...@googlegroups.com

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

TH Lim

unread,
Jun 12, 2012, 1:51:46 AM6/12/12
to singapore-functi...@googlegroups.com
Friday would be good, we can hang out longer. However, if it is on Wed, I try to make it.

Mike Mazur

unread,
Jun 12, 2012, 2:10:52 AM6/12/12
to singapore-functi...@googlegroups.com
Hi,

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

Sorry!
Mike

zan

unread,
Jun 12, 2012, 2:30:51 AM6/12/12
to singapore-functi...@googlegroups.com
is {new context} available on thursday?

Mike Mazur

unread,
Jun 12, 2012, 3:10:59 AM6/12/12
to singapore-functi...@googlegroups.com
Hi,

Thursday should be fine. 

Mike

Dr. ÉRDI Gergő

unread,
Jun 20, 2012, 3:55:04 AM6/20/12
to singapore-functi...@googlegroups.com

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

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

G

Mike Mazur

unread,
Jun 20, 2012, 9:18:51 AM6/20/12
to singapore-functi...@googlegroups.com
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

Dr. ERDI Gergo

unread,
Jun 20, 2012, 9:20:20 AM6/20/12
to singapore-functi...@googlegroups.com
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

Dr. ÉRDI Gergő

unread,
Jun 24, 2012, 9:27:41 PM6/24/12
to singapore-functi...@googlegroups.com

Hi,

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

Thanks,
Gergo

Mike Mazur

unread,
Jun 24, 2012, 11:37:49 PM6/24/12
to singapore-functi...@googlegroups.com
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

Lu Zhuo Ming

unread,
Jun 25, 2012, 7:31:33 AM6/25/12
to singapore-functi...@googlegroups.com
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

Raymond

unread,
Jun 25, 2012, 7:53:00 AM6/25/12
to singapore-functi...@googlegroups.com, singapore-functi...@googlegroups.com
28 June instead of July or was there a change in date?

Dr. ÉRDI Gergő

unread,
Jun 25, 2012, 7:54:27 AM6/25/12
to singapore-functi...@googlegroups.com

June. This Thursday.

Chien Nguyen

unread,
Jun 25, 2012, 9:19:49 AM6/25/12
to singapore-functi...@googlegroups.com
Thanks.

Lu Zhuo Ming

unread,
Jun 28, 2012, 11:47:11 AM6/28/12
to singapore-functi...@googlegroups.com
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

Mike Mazur

unread,
Jun 28, 2012, 7:29:05 PM6/28/12
to singapore-functi...@googlegroups.com
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

Lu Zhuo Ming

unread,
Jun 28, 2012, 7:57:19 PM6/28/12
to singapore-functi...@googlegroups.com
July 25 is good for me. :)

Dr. ERDI Gergo

unread,
Jul 1, 2012, 6:50:03 AM7/1/12
to singapore-functi...@googlegroups.com
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

Mike Mazur

unread,
Jul 1, 2012, 8:40:30 AM7/1/12
to singapore-functi...@googlegroups.com
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

Dr. ÉRDI Gergő

unread,
Jul 2, 2012, 9:24:40 PM7/2/12
to singapore-functi...@googlegroups.com

Ok so I just checked, 26th looks doable.

Reply all
Reply to author
Forward
0 new messages