CIS 890 E-mail Archive


From: Alley Stoughton <stough@cis.ksu.edu>
Date: Wed, 7 Jan 2009 15:31:27 -0600
Subject: [890] reminder: enrollment and meeting day/time

Hi Jason, Jon and Matt,

I just wanted to remind you to enroll in CIS 890 (reference: 16084),
and that the class will meet on Fridays from 1:30-3:30 in N236 (the
Conference Room), beginning January 16.  The course website is

  http://people.cis.ksu.edu/~stough/890/

Cheers,

Alley

From: Alley Stoughton <stough@cis.ksu.edu>
Date: Tue, 13 Jan 2009 15:40:58 -0600
Subject: [890] reading assignment for Friday's class 

I've put a reading assignment for Friday's class on the course website:

  http://people.cis.ksu.edu/~stough/890/

We won't cover all of this material in class on Friday.  In fact,
we'll take things as slowly as we need to.  But you should at least
start reading and thinking about it before class.

See you at 1:30 on Friday!

Alley

From: Alley Stoughton <stough@cis.ksu.edu>
Date: Sat, 24 Jan 2009 17:13:59 -0600
Subject: [890] output coverage 

I did some reading in the Twelf User's Guide about output coverage,
and realized that it's not intended to deal with examples in which
output coverage is across multiple constants.  Instead, it seems to be
on a constant-by-constant basis.  When an output isn't a variable,
this will only succeed when the kinding of the judgment forces terms
of the type of the output to have a certain form.

I came up with a simple example of this, although not an especially
useful one, and it's included below.  We'll see something more useful
when we get to Part 2 of our introduction, but if anyone can come up
with a more useful one now, please share it with the rest of us.

Alley

-----------------------------------------------------------------------------

% output coverage example involving non-variable

nat : type.
z : nat.
s : nat -> nat.

even : nat -> type.

even-z : even z.
even-s : {N : nat} even N -> even (s(s N)).

foo : {N1 : nat} even N1 -> even (s(s N1)) -> type.

%mode foo +N1 +D1 -D2.

foo' : {N1 : nat} {D1: even N1} foo N1 D1 (even-s N1 D1).

%worlds () (foo _ _ _).

%total D1 (foo N1 D1 D2).

goo : {N1 : nat} even N1 -> even N1 -> type.

%mode goo +N1 +D1 -D2.

%{

output coverage OK for premise

  foo N1 D1 (even-s N1 D2)

of goo', even though

  even-s N1 D2

is not a variable.  This is because kinding of foo means that foo's
output must be derivation of even (s(s N1)), and so must have
form even-s N1 D2 for some D2.  (Of course, this D2 will always
be D1, and so goo could be defined directly, without using foo.)

}%

goo' :
  {N1 : nat} {D1 : even N1} {D2 : even N1}
  foo N1 D1 (even-s N1 D2) -> goo N1 D1 D2.

%worlds () (goo _ _ _).

%total D1 (goo N D1 D2).

%solve D : goo (s(s(s(s z)))) (even-s (s(s z)) (even-s z even-z)) D2.

From: Alley Stoughton <stough@cis.ksu.edu>
Date: Thu, 12 Mar 2009 16:39:07 -0500
Subject: [890] plan for class tomorrow 

Hi Twelf'ers,

I just wanted to remind you that, from tomorrow until the end of the
semester, you need to be working on your projects, and giving status
reports about how you are progressing.  You can also talk about other
interesting things that you learn along the way.  Tomorrow, I hope to
hear about what you are thinking of doing for your projects.

Alley

From: Alley Stoughton <stough@cis.ksu.edu>
Date: Fri, 13 Mar 2009 15:58:22 -0500
Subject: [890] example from today's class now online

I've put the example from today's class -- proving determinism of
evaluation for the untyped lambda calculus -- on the course website.

I look forward to hearing how your Twelf projects are going when
we return after the spring break.

Regards,

Alley

From: Alley Stoughton <stough@cis.ksu.edu>
Date: Fri, 10 Apr 2009 09:48:42 -0500
Subject: [890] Midwest Programming Languages Day at KU

On the last day of the semester, there will be a Midwest Programming
Languages Day at KU:

  http://www.ittc.ku.edu/~andygill/proglangday.php

I hope you'll all consider going, and perhaps even proposing a talk.

We won't have class on that day.  We'll schedule a day/time during
finals week for everyone to give presentations about their Twelf
projects.

Alley

From: Alley Stoughton <stough@cis.ksu.edu>
Date: Fri, 10 Apr 2009 22:52:23 -0500
Subject: [890] open house next week -- no class 

Ah, I didn't realize in class today that next week is the day
before open house, when we'll all be told that there are to
be no classes.  But if you want to talk about your projects next
week, you can always come see me individually.

Alley

From: Alley Stoughton <stough@cis.ksu.edu>
Date: Thu, 16 Apr 2009 23:47:44 -0500
Subject: [890] reminder: no class tomorrow 

Hi Folks,

Just a reminder that there is no class tomorrow (Friday).  Classes
are supposed to be canceled for open house.

Alley

From: Alley Stoughton <stough@cis.ksu.edu>
Date: Fri, 24 Apr 2009 16:50:40 -0500
Subject: [890] scheduling project talks

Hi Twelfers,

Ideally, I'd like to schedule the Twelf project talks for the morning
of Thursday, May 14 -- the Thursday of finals week.  We'll have 45
minute talks/demos.  Please let me know when you're available during
the interval between 9:30 and 1:30 on that day.

Thanks!

Alley

PS Remember that we'll only meeting one more time at our usual
Friday time -- next week (the 1st).

From: Alley Stoughton <stough@cis.ksu.edu>
Date: Fri, 1 May 2009 14:48:29 -0500
Subject: [890] timetable for project presentations 

Here's a tentative schedule for the Twelf project presentations,
on Thursday, May 14:

   9:30 - 10:15  Andrew
  10:30 - 11:15  Matt
  11:30 - 12:15  Jon
  12:30 -  1:15  Jason

Each presentation should be about 45 minutes long, including questions,
but if they spill over a bit, that's OK.

If your time doesn't work for you, please let me know ASAP.  I hope
that you'll come hear what your fellow students have done, but it's
not obligatory.

Cheers,

Alley

From: Alley Stoughton <stough@cis.ksu.edu>
Date: Mon, 11 May 2009 16:14:54 -0500
Subject: [890] project presentations on Thursday

Hi Twelfers,

I've booked the CIS Library for the Twelf project presentations
on Thursday:

   9:30 - 10:15  Andrew
  10:30 - 11:15  Matt
  11:30 - 12:15  Jon

See you then!

Alley

Alley Stoughton (Alley.Stoughton@gmail.com)