 Robert Harper: Types and Programming Languages
started 10/15/2002; 5:33:31 AM - last post 10/17/2002; 5:47:57 AM
|
|
Ehud Lamm - Robert Harper: Types and Programming Languages 
10/15/2002; 5:33:31 AM (reads: 1879, responses: 7)
|
|
| Robert Harper: Types and Programming Languages |
|
Scottfest 2002: Types and Programming Languages. Carnegie Mellon University, October, 2002.
A highly theoretical talk given in honor of Dana Scott. Constructive validity, constructivism in general, and how Dana Scott's work initiated the type-theoretic study of programming languages.
This talk would have a made a great paper. The slides are a bit too dense for mortals.
One great quote: Logical type theory is the GUT of PL’s!
Alas, I could only find PPT slides.
Posted to theory by Ehud Lamm on 10/15/02; 5:36:05 AM
|
|
|
|
Kimberley Burchett - Re: Robert Harper: Types and Programming Languages
10/16/2002; 8:10:06 AM (reads: 869, responses: 0)
|
|
|
I can tell there are a lot of interesting connections in this presentation, but the syntax is completely foreign to me. For example, the colon in "C, :W, P" clearly means something. Does anybody know of a quick-reference or backgrounder for the notation?
|
|
Frank Atanassow - Re: Robert Harper: Types and Programming Languages
10/16/2002; 9:24:17 AM (reads: 847, responses: 1)
|
|
You must be talking about the slide on substructural systems. I think you are missing some fonts which Harper used, since
- on my Windows machine that colon is a logical negation sign (\neg, \urcorner in LaTeX), and
- I noticed some funny characters on other slides which are obviously wrong.
The name of the font for the colon/negation is "cmsy10"; I forget where I found it, but I had it installed. Other funny characters, which presumably are intended to be logical conjunction (\wedge) and disjunction (\vee), appear on an earlier slide titled Constructions and Types. For some reason PowerPoint says these are also cmsy10 characters, so maybe my font version is different or older than Harper's too.
Anyway, with those provisos, the notation looks pretty standard to me.
|
|
Ehud Lamm - Re: Robert Harper: Types and Programming Languages
10/16/2002; 9:26:46 AM (reads: 894, responses: 0)
|
|
|
Yes. I wans't sure which fonts are missing exactly, but with some effot I managed to understand the formulas.
|
|
Frank Atanassow - Re: Robert Harper: Types and Programming Languages
10/16/2002; 9:32:05 AM (reads: 868, responses: 0)
|
|
|
OK, I think I got cmsy10 from the
Mozilla MathML fonts page.
A Google search for cmsy10.ttf turned up some other sources also.
|
|
Frank Atanassow - Re: Robert Harper: Types and Programming Languages
10/16/2002; 9:48:23 AM (reads: 855, responses: 0)
|
|
|
Oh and, BTW, it's a nice talk. :) It gives a crash tour of type (in)dependence, classical and substructural logic and suggests how they impinge on programming languages.
|
|
Kimberley Burchett - Re: Robert Harper: Types and Programming Languages
10/16/2002; 11:00:48 AM (reads: 830, responses: 0)
|
|
|
What a difference a font makes! I now have universal and existential quantifiers, logical negation, subset, superset, morphism arrows, top, bottom, entailment, etc. Thanks! :)
One character is still eluding me though -- In the first "Control operators" slide, on the third line that starts "Equivalently, EM...", I see a circumflected capital letter C between the two phi. Anybody know what it is?
|
|
Frank Atanassow - Re: Robert Harper: Types and Programming Languages
10/17/2002; 5:47:57 AM (reads: 771, responses: 0)
|
|
|
I haven't looked at that particular slide, but I remember the circumflected C showed up for one of the logical conjunction and disjunction; I think the other was a "combined AE".
|
|
|
|