ature but it is semantically meaningless.
>
> Thorsten
>
> From: Jon Sterling
> Date: Monday, 29 January 2024 at 08:24
> To: Thorsten Altenkirch (staff)
> Cc: types-list@LISTS.SEAS.UPENN.EDU
> Subject: Re: [TYPES] a naive question on datatype declarations
>
> T
to confuse the two things.
>
> Cheers,
> Thorsten
>
> From: Types-list <mailto:types-list-boun...@lists.seas.upenn.edu>> on behalf of Jon Sterling
> mailto:j...@jonmsterling.com>>
> Date: Saturday, 27 January 2024 at 15:25
> To: types-list@LISTS.SEAS.UPENN.EDU <mailto:
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Hi Gershom,
This is a good question, and often overlooked. Bob Harper taught me to think of
these things as abstract types, and I agree — so the thing that makes two
different datatype declarations different is the
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Hi all,
I am seconding Neel's concern, and wish to thank him for bringing it up. After
much agonising, I have chosen not to go to POPL at all this year despite the
fact that I have ***two papers*** in the conference;
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Dear Andrej,
I am not completely sure because it is a while since I had watched this, but I
think this might be related to the topic of Per Martin-Löf's 2013 Earnest Nagel
Lecture “Invariance Under Isomorphism and
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
I think I have also heard 'contractum'. But maybe that refers to the result of
applying a single reduction rule? Not sure.
Best,
Jon
On Thu, Jun 9, 2022, at 5:10 PM, Hendrik Boom wrote:
> [ The Types Forum,
ught topic and that people have
good reasons for holding the views they do. I hope that as a community we can
find a way to talk about it that is respectful and also cognizant of the
difficulty of the issues that we are facing now.
Best wishes,
Jon Sterling
> On Mar 9, 2022, at 5:07 PM, Fritz He
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Neel, thank you for bringing this to the community's attention. I think this is
terrible --- and it shows the way that certain European conference organizers
divide up imperialist wars of aggression and colonization
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
I am very sorry to say that Kevin Watkins has passed away in May of last year.
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
I think it is confusing to refer to costs that are already paid by someone else
as "a bill that someone needs to foot". arXiv already exists, etc. and
anyone who wants to make a new totally free journal does not
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
I want to put in my agreement with Talia's second point that we should move to
a model in which deadlines are frequent and cheap to miss (as is the case in
every discipline that is lucky enough to be based on journals)
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Dear Andrej and Thomas,
I was referring to extensional MLTT (MLTT 1979), not intensional MLTT
(for which the question is still open, I believe); I believe the result
is from Troelstra, but I can try and dig up the
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
(Sorry, please read the first sentence as “from an *untyped* computation
system not typed.
-JMS
On Wed, Nov 5, 2014, at 09:01 AM, Jon Sterling wrote:
Eduardo,
I would say that the kind of thing you are thinking
13 matches
Mail list logo
