Re: [TYPES] TaPL Course?

2022-12-21 Thread Spertus, Mike 
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Robert and I have discussed this offline, but in case it is of interest to 
others, I have a GitHub repo that repackages the implementations from the 
course site as Dune projects and adds a REPL for playing with the type checkers 
interactively at 
https://urldefense.com/v3/__https://github.com/mspertus/TAPL__;!!IBzWLUs!WrDNkB_Fzfrh4n4XyZK8KHIa1TZ35D0kDmXEjGRX9gqD8L4mt1_BrWO6vIQhcVCnKYHHEY-fS8kf1hORutvxCPQb-x-0$
 . You can use them directly on machines with ocaml and Dune 3 or use the 
included devfile to create a preconfigured development container if you don't 
want to mess around with installing prerequisites. The readme includes copious 
usage instructions.

Mike

-Original Message-
From: Types-list  On Behalf Of Frank 
Pfenning
Sent: Tuesday, December 20, 2022 1:15 PM
To: Robert Rand 
Cc: Types list 
Subject: RE: [EXTERNAL][TYPES] TaPL Course?



[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hi Robert,

  You might be interested in the "Types and Programming Languages"
<https://urldefense.com/v3/__http://www.cs.cmu.edu/*fp/courses/15814-f21/__;fg!!IBzWLUs!XziYgKa-Uuca8ko4fRdlXlt_RzXFJBsybnlrX-d7qMvvr5KsG9NJaW6KIlYKfNHYdOZzVfy3djmP8cHwhRlY3S0$
 > course we teach at CMU, for which I have written extensive notes that 
complement the textbook "Practical Foundations of Programming Languages"
by Bob Harper.  I also have a small implementation of a core language Lambda 
(which I am happy to share) so students can write, type-check, and run some 
concrete examples.  The course is specifically designed as a "breadth" course 
in that it does not presuppose any prior experience in functional programming.

  - Frank

On Sat, Dec 17, 2022 at 3:19 AM Robert Rand  wrote:

> [ The Types Forum, 
> http://lists.seas.upenn.edu/mailman/listinfo/types-list
> ]
>
> Hi,
>
> I was wondering who is teaching a programming languages course using 
> Types and Programming Languages? I'm planning on teaching such a 
> course at UChicago this Spring (March - June) and I'm looking for 
> inspiration and suggestions. If you're on the quarter system and/or 
> have material you'd like to share, that's especially welcome!
>
> Thanks!
> Robert
>


--
Frank Pfenning, Professor
Computer Science Department
Carnegie Mellon University
Pittsburgh, PA 15213-3891

https://urldefense.com/v3/__http://www.cs.cmu.edu/*fp__;fg!!IBzWLUs!XziYgKa-Uuca8ko4fRdlXlt_RzXFJBsybnlrX-d7qMvvr5KsG9NJaW6KIlYKfNHYdOZzVfy3djmP8cHwsVPsMfs$
+1 412 268-6343
GHC 6017

Re: [TYPES] TaPL Course?

2022-12-20 Thread Frank Pfenning 
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hi Robert,

  You might be interested in the "Types and Programming Languages"

course we teach at CMU, for which I have written extensive notes that
complement the textbook "Practical Foundations of Programming Languages"
by Bob Harper.  I also have a small implementation of a core language
Lambda (which I am happy to share) so students can write, type-check,
and run some concrete examples.  The course is specifically designed
as a "breadth" course in that it does not presuppose any prior experience
in functional programming.

  - Frank

On Sat, Dec 17, 2022 at 3:19 AM Robert Rand  wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
> ]
>
> Hi,
>
> I was wondering who is teaching a programming languages course using Types
> and Programming Languages? I'm planning on teaching such a course at
> UChicago this Spring (March - June) and I'm looking for inspiration and
> suggestions. If you're on the quarter system and/or have material you'd
> like to share, that's especially welcome!
>
> Thanks!
> Robert
>


-- 
Frank Pfenning, Professor
Computer Science Department
Carnegie Mellon University
Pittsburgh, PA 15213-3891

https://urldefense.com/v3/__http://www.cs.cmu.edu/*fp__;fg!!IBzWLUs!XziYgKa-Uuca8ko4fRdlXlt_RzXFJBsybnlrX-d7qMvvr5KsG9NJaW6KIlYKfNHYdOZzVfy3djmP8cHwsVPsMfs$
 
+1 412 268-6343
GHC 6017

Re: [TYPES] TaPL Course?

2022-12-20 Thread Andreas Nuyts 

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Dear Robert,

We have a Formal Systems course based on TAPL at KU Leuven.
In 2 practical sessions, the students learn how to use Agda and in the 
third, they formalize Typed Arithmetic:
https://urldefense.com/v3/__https://github.com/anuyts/agda-sessions__;!!IBzWLUs!VVdQCimkUObVjDW1CI1V2_kcHewEmae7Ry_alrqCQq6XESgAi54MWeKWEj0mO12hy2avYusU0aEvQachzxrmpFnznjbhMvi3JQ$ 
There's also a course project. It used to be a formalization of various 
extensions of the STLC but now we're formalizing Web Assembly instead.


Best,
Andreas Nuyts

On 01.12.22 06:49, Robert Rand wrote:

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hi,

I was wondering who is teaching a programming languages course using Types
and Programming Languages? I'm planning on teaching such a course at
UChicago this Spring (March - June) and I'm looking for inspiration and
suggestions. If you're on the quarter system and/or have material you'd
like to share, that's especially welcome!

Thanks!
Robert

Re: [TYPES] TaPL Course?

2022-12-17 Thread Alejandro Díaz-Caro 
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hi Robert,

I give a course at a degree in programming at Quilmes University, using
typed lambda calculus.

The webpage and notes (in Spanish) is here:
https://urldefense.com/v3/__http://clp.web.unq.edu.ar/apuntes-y-practicas/__;!!IBzWLUs!XAPllmUn3YsWKjEpx23e80cVtUf6jfRHZp_x1BoCh6HDYQI2H6l5-PdbaijzRqcyEpv0KoEUIJVYhC1Mg4-z_tXDECi_9hmGGn4L$
 

However, the notes are mostly based on the following very nice book:

G. Dowek & J.-J. Levy, Introduction to the theory of programming languages,
Springer, 2011

Fell free to use the exercises or any material if it suits the topics you
plan to cover.

Best,
Alejandro

--
Sent from my mobile (i.e. sorry for the bad autocorrections)

El sáb, 17 dic. 2022 05:20, Robert Rand  escribió:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
> ]
>
> Hi,
>
> I was wondering who is teaching a programming languages course using Types
> and Programming Languages? I'm planning on teaching such a course at
> UChicago this Spring (March - June) and I'm looking for inspiration and
> suggestions. If you're on the quarter system and/or have material you'd
> like to share, that's especially welcome!
>
> Thanks!
> Robert
>

[TYPES] TaPL Course?

2022-12-17 Thread Robert Rand 
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hi,

I was wondering who is teaching a programming languages course using Types
and Programming Languages? I'm planning on teaching such a course at
UChicago this Spring (March - June) and I'm looking for inspiration and
suggestions. If you're on the quarter system and/or have material you'd
like to share, that's especially welcome!

Thanks!
Robert