[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Thanks for taking the trouble to point that out, Lindsay! It's good to be
reminded how easy it is for any of us (well, many of us, anyway :-) to slip
into unintentionally hurtful or excluding figures of speech.
-
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
(… and sorry for mis-typing your name in the process of thanking you!)
On Apr 22, 2013, at 1:51 PM, "Benjamin C. Pierce"
wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listin
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
A colleague asked me an interesting question recently:
Can the Chomsky hierarchy (regular grammars, context-free, context-sensitive,
Turing-complete) be phrased in terms that functional programmers would find
natural,
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Many thanks, Dimitrios, for the great job you’ve done over the past three
years! The Types list is an important resource for the community, and your
stewardship has been much appreciated.
And thanks to Gabriel for ste
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Dear Types types,
What is the best presentation of the continuation-passing transform and its
proof of correctness (“best” in the sense of clarity of both algorithm and
proof, not efficiency or generality)?
Many thank
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Those who still feel the loss of Martin's passing may want to know about a
memorial talk on his life and work from LICS in July.
Video: https://www.youtube.com/watch?v=WpWt40l_uDk
Slides only: http://www.cis.upenn.edu/~
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Impredicativity is also useful in type-theoretic encodings of objects. Objects
with method interface M are represented as elements of
Obj(M) = Exists X, X * (X -> M(X))
i.e., as pairs of a “hidden state” X and a
going in the
> form of Zoom webinars.
>
> There is also the potential of coming up with new publication models. My
> long-standing pet peeve, for example, has been the question why most proof
> assistants do not have anything remotely comparable to Isabelle's Archive of
> For
