[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
I also find this utterly wrong, and we (a group of computer scientists working in Austria + collaborators) already started an initiative to change this. I am still waiting for news from the person who is talking to the ETAPS chair(s). Best, Ana On Tue, Mar 8, 2022 at 8:01 PM <types-list-requ...@lists.seas.upenn.edu> wrote: > Send Types-list mailing list submissions to > types-list@LISTS.SEAS.UPENN.EDU > > To subscribe or unsubscribe via the World Wide Web, visit > https://LISTS.SEAS.UPENN.EDU/mailman/listinfo/types-list > or, via email, send a message with subject or body 'help' to > types-list-requ...@lists.seas.upenn.edu > > You can reach the person managing the list at > types-list-ow...@lists.seas.upenn.edu > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Types-list digest..." > > > Today's Topics: > > 1. Request: Papers to understand Nordic logic talk (Julin S) > 2. Re: Request: Papers to understand Nordic logic talk > (Rishiyur Nikhil) > 3. Consistency of NF (Jamie) > 4. ETAPS bars Russian researchers from attending (Neel Krishnaswami) > 5. Re: ETAPS bars Russian researchers from attending (Talia Ringer) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Sat, 19 Feb 2022 09:45:19 +0530 > From: Julin S <julinshaj...@gmail.com> > To: types-list@lists.seas.upenn.edu > Subject: [TYPES] Request: Papers to understand Nordic logic talk > Message-ID: > < > camvfptuj5wzzftud+d0uzvqabxhgbhhbniqorn_qoworgou...@mail.gmail.com> > Content-Type: text/plain; charset="UTF-8" > > Hi. I saw in the types-announce[2] mailing list about a talk by Thierry > Coquand > as part of the Nordic Online Logic Seminar. > > I'm sort of new to logic and type theory and was trying to find papers that > would help me understand the talk better. > > The abstract was: > > > > The first part will be about representation of mathematics on a > > computer.Questions that arise there are naturally reminiscent of issues > that > > arise when teaching formal proofs in a basic logic course, e.g. how to > deal > > with free and bound variables, and instantiation rules. As discussed in > a 1962 > > paper of Tarski, these issues are "clearly experienced both in teaching > an > > elementary course in mathematical logic and in formalizing the syntax of > > predicate logic for some theoretical purposes." I will present two quite > > different approaches to this problem: one inspired by Tarski's paper (N. > > Megill, system Metamath) and one using dependent type theory (N.G. de > Bruijn). > > > > The second part will then try to explain how notations introduced by > dependent > > type theory suggest new insights for old questions coming from Principia > > Mathematica (extensionality, reducibility axiom) through the notion of > > universe, introduced by Grothendieck for representing category theory in > set > > theory, and introduced in dependent type theory by P. Martin-L?f. > > > Could anyone help me find the papers/works that this abstract may be > referring > to (and anything else that can be helpful to better understand the talk)? > > I tried searching for these on google scholar but couldn't pinpoint the > papers. > > - 1962 paper by Tarksi > - Tarski's paper (N. Megill, system Metamath) > - dependent type theory (N. G. de Bruijn) > > Could metamath be this[1]? > > [1]: > https://urldefense.com/v3/__http://us.metamath.org/downloads/metamath.pdf__;!!IBzWLUs!GgCWS35KVAXOBGITv9G363gRbkyb18vD4--hSnWLV-gywkE2s4FtPjLKBnsWe-MrlCqCOSshYmI$ > [2]: http://lists.seas.upenn.edu/pipermail/types-announce/2022/010050.html > > Thanks and regards, > Julin Shaji > > > ------------------------------ > > Message: 2 > Date: Sat, 19 Feb 2022 19:03:07 -0500 > From: Rishiyur Nikhil <nik...@acm.org> > To: Julin S <julinshaj...@gmail.com> > Cc: Types list <types-list@lists.seas.upenn.edu> > Subject: Re: [TYPES] Request: Papers to understand Nordic logic talk > Message-ID: > < > caodmajrvtof_-bc8jfd1js-tvf78h2qrkqjmkt62h2bgfg0...@mail.gmail.com> > Content-Type: text/plain; charset="UTF-8" > > Also of interest, apropos this topic: > > @article{ > Buzzard2021, > author = "Buzzard, Kevin", > title = "What is the Point of Computers? A Question for Pure > Mathematicians", > note = "arXiv:2112211598v1 [math.HO] 22-Dec 2021" > year = 2021, > month = "December 22", > annote = " > https://urldefense.com/v3/__https://arxiv.org/abs/2112.11598__;!!IBzWLUs!AxV2Fv4-shJoZ8gpbEEqqyhh5PvOj9MVC_4H9O8cSQzUmEEaXjVPbmfeHkiRyqSn_-uarZItZ_8$ > " > } > > Nikhil > > > ------------------------------ > > Message: 3 > Date: Tue, 1 Mar 2022 06:28:59 +0000 > From: Jamie <bellissimogio...@gmail.com> > To: types-list@lists.seas.upenn.edu > Subject: [TYPES] Consistency of NF > Message-ID: > <CA+0Xc9= > su2iyqbqipqrn26430pir+1evwo5lg5-v4bofzzo...@mail.gmail.com> > Content-Type: text/plain; charset="UTF-8" > > Some of you may know that I've been working on the consistency of Quine's > NF for a few years. NF is a foundational system which can be presented > both as a type theory and a set theory, and of which it is not easy to > prove consistency. > > I've been developing a new angle, which I've posted here: > > https://urldefense.com/v3/__https://arxiv.org/pdf/1406.4060.pdf__;!!IBzWLUs!B0Pb7f_Vb3l9XE9Ze0En6kKg0h1rNrw4AbkLo3jzwf6UPt2a2JoVMLPH4OrVkbnqJnYd0pL6fHY$ > > This has been looked at by at least one person other than myself without > exposing major flaws so far, and I'm taking the liberty of drawing this to > the attention of TYPES because I feel the argument could now be usefully > examined by this broader community, in the hope that we can confirm it as > correct, or refine it if required. > > I welcome questions and comments. Thanks in advance. > > Jamie > > > ------------------------------ > > Message: 4 > Date: Tue, 8 Mar 2022 15:01:09 +0000 > From: Neel Krishnaswami <neelakantan.krishnasw...@gmail.com> > To: types-list@lists.seas.upenn.edu > Subject: [TYPES] ETAPS bars Russian researchers from attending > Message-ID: <ee84e94a-6cd7-9b0c-a228-d0c8f5c1e...@gmail.com> > Content-Type: text/plain; charset=UTF-8; format=flowed > > The ETAPS website ( > https://urldefense.com/v3/__https://www.etaps.org__;!!IBzWLUs!HUevd2N5Ms-2WYC1sMdH93ef4xxRy4BjZ9KD0I8SPwLGGpv-Rk7u_Emgl9qMMyLGK4ex90o0Cm0$ > ) has the following text on its > front page: > > > The ETAPS association strongly condemns the war against Ukraine > > launched by President Putin. It is an intolerable breach of > > international law and a crime against humanity, unfolding in Europe > > now. Therefore,?until further notice, ETAPS 2022 cannot accept > > registrations from affiliates of Russian research institutions or > > companies. > > While I'm as opposed to illegal wars of aggression as anyone else, this > feels like a serious mistake. > > There are many Russians (such as Jetbrains corporation) who have taken > the serious personal risk of publically opposing the war, and barring > them from our conferences due to their nationality feels wrong to me. > > It may well be that the financial sanctions regime means that > registration payments cannot be accepted, but that is quite different > from barring them personally. > > What do the rest of you think? > > Best, > Neel > > > ------------------------------ > > Message: 5 > Date: Tue, 8 Mar 2022 12:55:33 -0600 > From: Talia Ringer <trin...@cs.washington.edu> > To: Neel Krishnaswami <neelakantan.krishnasw...@gmail.com> > Cc: types-list@lists.seas.upenn.edu > Subject: Re: [TYPES] ETAPS bars Russian researchers from attending > Message-ID: > < > cafd6xs9ooc8hw8kvrgkj3odmeb5okdfab+nubwtzwa378t+...@mail.gmail.com> > Content-Type: text/plain; charset="UTF-8" > > 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 ACM Ethics Code and other relevant ethical codes. > > Sanctions make a lot of sense as a way of pressuring a country to cease > unwarranted behavior, and pushing citizens to resist governments engaging > in those behaviors. But academic boycotts are uniformly wrong. This is > especially true given that academics in Russia are overwhelmingly > anti-Putin and are often active in resisting the government even when it is > literally illegal to do so. > > Russian politics are about as divided as American politics. It is not OK to > conflate governments with people. > > It is also not really an action that accomplishes anything, unlike > sanctions. So if we want to accomplish something as a community, we can do > a lot, like: > > 1. organize large donation efforts to help with relief in Ukraine and > resettlement if refugees, > 2. personally reach out to those in and outside of our community who are > impacted, and ask if they need anything, > 3. organize a group effort to call our representatives and demand > additional support for Ukraine and acceptance of refugees, and explain how > we will personally help with that effort, > 4. talking to our Russian friends who are organizing against Putin, and > helping them with that effort, > 5. talking to Russians who are confused and unsure of what is true, and > explaining the truth, > 6. funding VPN access for Russians who want to continue to access > independent news that will help them resist. > > Here's a reputable organization I like, if anyone wants to donate: > > https://urldefense.com/v3/__https://novaukraine.org/__;!!IBzWLUs!DHlXVoZ6BDwBfH2OIWb-MM7tsQ8m5xqm0-qPznoFXvlpDYMV2qsTpSP8ZkB_53Xdvhwvm4JgIak$ > > Sanctions tend to work best when there is also an allied resistance > movement within the country; this was certainly true in South Africa, and > it's certainly true in Russia, too. It works to Putin's advantage to > completely isolate those in Russia who are our allies. It comes across as > performative, too, and it's against the ethics code. > > We should stand against all forms of academic boycott. But if anyone makes > comments that are very harmful to Ukrainian researchers, or puts them at > risk, of course we should enforce that through the ethics codes and codes > of conduct as well. And we should support Ukraine during this time; there > is no apolitical stance in war, especially a war this unprompted. But > banning Russian academics is definitely not the way to do that. > > Talia > > On Tue, Mar 8, 2022, 12:33 PM Neel Krishnaswami < > neelakantan.krishnasw...@gmail.com> wrote: > > > [ The Types Forum, > http://lists.seas.upenn.edu/mailman/listinfo/types-list > > ] > > > > The ETAPS website ( > > > https://urldefense.com/v3/__https://www.etaps.org__;!!IBzWLUs!HUevd2N5Ms-2WYC1sMdH93ef4xxRy4BjZ9KD0I8SPwLGGpv-Rk7u_Emgl9qMMyLGK4ex90o0Cm0$ > > ) has the following text on its > > front page: > > > > > The ETAPS association strongly condemns the war against Ukraine > > > launched by President Putin. It is an intolerable breach of > > > international law and a crime against humanity, unfolding in Europe > > > now. Therefore, until further notice, ETAPS 2022 cannot accept > > > registrations from affiliates of Russian research institutions or > > > companies. > > > > While I'm as opposed to illegal wars of aggression as anyone else, this > > feels like a serious mistake. > > > > There are many Russians (such as Jetbrains corporation) who have taken > > the serious personal risk of publically opposing the war, and barring > > them from our conferences due to their nationality feels wrong to me. > > > > It may well be that the financial sanctions regime means that > > registration payments cannot be accepted, but that is quite different > > from barring them personally. > > > > What do the rest of you think? > > > > Best, > > Neel > > > > > ------------------------------ > > Subject: Digest Footer > > _______________________________________________ > Types-list mailing list > Types-list@LISTS.SEAS.UPENN.EDU > https://LISTS.SEAS.UPENN.EDU/mailman/listinfo/types-list > > > ------------------------------ > > End of Types-list Digest, Vol 140, Issue 1 > ****************************************** >
