[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Thanks, Alex. Reading that prompted me to reach out to my programming
languages friends in Russia and check on them. Indeed a number have fled
the country already, and are currently out of work, and have family stuck
in
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Yes, there was an academic boycott on South Africa. And the general
consensus in retrospect by scholars of South Africa is that it accomplished
nothing beyond sanctions except for "sending a message," and again at the
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
I agree this is a bad move. Ever since JetBrains' statement against the
Russian invasion of Ukraine, I've been proud to continue to collaborate
with them. Furthermore, discrimination based on national origin is against
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Since I complained as last year about this, I've joined on the SPLASH
hybridization committee. My understanding so far is:
- there are some hidden costs
- overcharging some people acts as a subsidy for other people who
consider them as operations running on an
> > actual computer, then we will have strong preferences!
> >
> > 4. A common source of confusion arises from the fact that if you have
> > a nice type-theoretic language (like the STLC), the
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> For example, if I write a proof in Agda, using function extensionality,
> is it a program? No. But if I write --cubical in the header of my Agda
> program and import a suitable cubical library, then yes. I can define
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Hi friends,
I have a strange discussion I'd like to start. Recently I was debating with
someone whether Curry-Howard extends to arbitrary logical systems---whether
all proofs are programs in some sense. I argued yes, he
e consume en gavage) and instead just go to lovely
> low-stress workshops and send my work periodically to journals, I would be
> so happy.
>
> Best,
> Jon
>
>
> On Sun, Aug 23, 2020, at 11:11 AM, Talia Ringer wrote:
> > [ The Types Forum,
> http://lists.seas.upenn.ed
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
I used to argue against changing conference deadline systems a lot, but the
pandemic response and political events in the US have made it clear to me
that this is a diversity issue. When a deadline is only once per year
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
I don't know about PLDI, but there are some costs associated with online
events. For example, automatic captioning software is still not very good
(Google's always turns "proofs" into "fruits" for me). Live captioning is
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Hello,
I have a question that has been bugging me for a long time, and I'm hoping
someone has some insight. I'm working in vanilla CIC, and right now I'm
interested in types "A : Type" and "B : I -> Type" for which
11 matches
Mail list logo
