[TYPES] Types-list Digest, Vol 140, Issue 1
Ana Sokolova
anas at cs.uni-salzburg.at
Wed Mar 9 01:42:18 EST 2022
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-request at lists.seas.upenn.edu>
wrote:
> Send Types-list mailing list submissions to
> types-list at 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-request at LISTS.SEAS.UPENN.EDU
>
> You can reach the person managing the list at
> types-list-owner at 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 <julinshaji01 at gmail.com>
> To: types-list at lists.seas.upenn.edu
> Subject: [TYPES] Request: Papers to understand Nordic logic talk
> Message-ID:
> <
> CAMVFpTUj5wzZftuD+d0UZvqABXHGBHhBniQORn_qoworGOU7uQ at 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 <nikhil at acm.org>
> To: Julin S <julinshaji01 at gmail.com>
> Cc: Types list <types-list at lists.seas.upenn.edu>
> Subject: Re: [TYPES] Request: Papers to understand Nordic logic talk
> Message-ID:
> <
> CAODMAjrVtof_-BC8JfD1js-TVF78h2qRKqjmkT62h2BGFg0U9Q at 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 <bellissimogiorno at gmail.com>
> To: types-list at lists.seas.upenn.edu
> Subject: [TYPES] Consistency of NF
> Message-ID:
> <CA+0Xc9=
> sU2iyQBQipqrN26430piR+1EVwo5Lg5-v4bofzzoMFQ at 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.krishnaswami at gmail.com>
> To: types-list at lists.seas.upenn.edu
> Subject: [TYPES] ETAPS bars Russian researchers from attending
> Message-ID: <ee84e94a-6cd7-9b0c-a228-d0c8f5c1e1db at 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 <tringer at cs.washington.edu>
> To: Neel Krishnaswami <neelakantan.krishnaswami at gmail.com>
> Cc: types-list at lists.seas.upenn.edu
> Subject: Re: [TYPES] ETAPS bars Russian researchers from attending
> Message-ID:
> <
> CAFD6Xs9OOc8hw8kvrGkJ3OdMeB5OkDFAb+NuBWTzWA378t+r_w at 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.krishnaswami at 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 at LISTS.SEAS.UPENN.EDU
> https://LISTS.SEAS.UPENN.EDU/mailman/listinfo/types-list
>
>
> ------------------------------
>
> End of Types-list Digest, Vol 140, Issue 1
> ******************************************
>
More information about the Types-list
mailing list