From jon at jonmsterling.com Sun Jan 2 15:19:40 2022 From: jon at jonmsterling.com (Jon Sterling) Date: Sun, 02 Jan 2022 21:19:40 +0100 Subject: [TYPES] =?utf-8?q?Wanted=3A_Jean-Yves_Girard=27s_=22Interpr?= =?utf-8?q?=C3=A9tation_fonctionnelle_et_=C3=A9limination_des_coupures_de_?= =?utf-8?b?bCdhcml0aG3DqXRpcXVlIGQnb3JkcmUgc3Vww6lyaWV1ciI=?= In-Reply-To: References: Message-ID: <90b9b6da-efb2-4956-bc55-1357dfffd24a@www.fastmail.com> I am very sorry to say that Kevin Watkins has passed away in May of last year. https://urldefense.com/v3/__https://www.asturner.com/obituaries/Kevin-Mark-Watkins?obId=21294662__;!!IBzWLUs!Ee08k8u04YKLxfzbGGztRaxj16VcgTsn82gmcVBxI0jjViWhAJhR2IfGcet1_BYZnCZfCPMDM3M$ Best wishes, Jon On Mon, Dec 27, 2021, at 6:51 PM, Cl?ment Aubert wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > > There are "bits and pieces" hosted at > > https://urldefense.com/v3/__https://www.cs.cmu.edu/*kw/scans/girard72thesis.pdf__;fg!!IBzWLUs!Ee08k8u04YKLxfzbGGztRaxj16VcgTsn82gmcVBxI0jjViWhAJhR2IfGcet1_BYZnCZfawtxZYw$ > > as presented at > > https://urldefense.com/v3/__https://www.cs.cmu.edu/*kw/scans.html__;fg!!IBzWLUs!Ee08k8u04YKLxfzbGGztRaxj16VcgTsn82gmcVBxI0jjViWhAJhR2IfGcet1_BYZnCZfvgAh6Qw$ > > Maybe you can ask Kevin Watkins for more and/or a source? > > > On 12/16/21 3:38 PM, Aaron Gray wrote: >> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] >> >> Jean-Yves Girard Ph.D thesis :- "Interpre?tation fonctionnelle et >> e?limination des coupures de l'arithme?tique d'ordre supe?rieur" >> >> Putting out the feelers for a copy of Jean-Yves Girard Ph.D thesis again. >> >> Regards, >> >> Aaron > > -- > Cl?ment Aubert, Assistant Professor of Computer Science, > School of Computer and Cyber Sciences, Augusta University, > https://urldefense.com/v3/__https://spots.augusta.edu/caubert/__;!!IBzWLUs!Ee08k8u04YKLxfzbGGztRaxj16VcgTsn82gmcVBxI0jjViWhAJhR2IfGcet1_BYZnCZfZV78LUo$ From Clement.Aubert at math.cnrs.fr Mon Jan 3 10:01:21 2022 From: Clement.Aubert at math.cnrs.fr (=?UTF-8?Q?Cl=c3=a9ment_Aubert?=) Date: Mon, 3 Jan 2022 10:01:21 -0500 Subject: [TYPES] =?utf-8?q?Wanted=3A_Jean-Yves_Girard=27s_=22Interpr?= =?utf-8?q?=C3=A9tation_fonctionnelle_et_=C3=A9limination_des_coupures_de_?= =?utf-8?b?bCdhcml0aG3DqXRpcXVlIGQnb3JkcmUgc3Vww6lyaWV1ciI=?= In-Reply-To: <90b9b6da-efb2-4956-bc55-1357dfffd24a@www.fastmail.com> References: <90b9b6da-efb2-4956-bc55-1357dfffd24a@www.fastmail.com> Message-ID: I am very sorry to read that he passed away, I was obviously not aware of this fact. My apologizes for this blunder. Thomas Seiller reported that he is hosting a copy at https://www.seiller.org/documents/Girard-phd.pdf It's even OCR'ed! On 1/2/22 3:19 PM, Jon Sterling wrote: > [ 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. https://urldefense.com/v3/__https://www.asturner.com/obituaries/Kevin-Mark-Watkins?obId=21294662__;!!IBzWLUs!Ee08k8u04YKLxfzbGGztRaxj16VcgTsn82gmcVBxI0jjViWhAJhR2IfGcet1_BYZnCZfCPMDM3M$ > > Best wishes, > Jon > > > On Mon, Dec 27, 2021, at 6:51 PM, Cl?ment Aubert wrote: >> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] >> >> >> There are "bits and pieces" hosted at >> >> https://urldefense.com/v3/__https://www.cs.cmu.edu/*kw/scans/girard72thesis.pdf__;fg!!IBzWLUs!Ee08k8u04YKLxfzbGGztRaxj16VcgTsn82gmcVBxI0jjViWhAJhR2IfGcet1_BYZnCZfawtxZYw$ >> >> as presented at >> >> https://urldefense.com/v3/__https://www.cs.cmu.edu/*kw/scans.html__;fg!!IBzWLUs!Ee08k8u04YKLxfzbGGztRaxj16VcgTsn82gmcVBxI0jjViWhAJhR2IfGcet1_BYZnCZfvgAh6Qw$ >> >> Maybe you can ask Kevin Watkins for more and/or a source? >> >> >> On 12/16/21 3:38 PM, Aaron Gray wrote: >>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] >>> >>> Jean-Yves Girard Ph.D thesis :- "Interpre?tation fonctionnelle et >>> e?limination des coupures de l'arithme?tique d'ordre supe?rieur" >>> >>> Putting out the feelers for a copy of Jean-Yves Girard Ph.D thesis again. >>> >>> Regards, >>> >>> Aaron >> -- >> Cl?ment Aubert, Assistant Professor of Computer Science, >> School of Computer and Cyber Sciences, Augusta University, >> https://urldefense.com/v3/__https://spots.augusta.edu/caubert/__;!!IBzWLUs!Ee08k8u04YKLxfzbGGztRaxj16VcgTsn82gmcVBxI0jjViWhAJhR2IfGcet1_BYZnCZfZV78LUo$ -- Cl?ment Aubert, Assistant Professor of Computer Science, School of Computer and Cyber Sciences, Augusta University, https://spots.augusta.edu/caubert/ From julinshaji01 at gmail.com Fri Feb 18 23:15:19 2022 From: julinshaji01 at gmail.com (Julin S) Date: Sat, 19 Feb 2022 09:45:19 +0530 Subject: [TYPES] Request: Papers to understand Nordic logic talk Message-ID: 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 From nikhil at acm.org Sat Feb 19 19:03:07 2022 From: nikhil at acm.org (Rishiyur Nikhil) Date: Sat, 19 Feb 2022 19:03:07 -0500 Subject: [TYPES] Request: Papers to understand Nordic logic talk In-Reply-To: References: Message-ID: 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 From bellissimogiorno at gmail.com Tue Mar 1 01:28:59 2022 From: bellissimogiorno at gmail.com (Jamie) Date: Tue, 1 Mar 2022 06:28:59 +0000 Subject: [TYPES] Consistency of NF Message-ID: 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 From neelakantan.krishnaswami at gmail.com Tue Mar 8 10:01:09 2022 From: neelakantan.krishnaswami at gmail.com (Neel Krishnaswami) Date: Tue, 8 Mar 2022 15:01:09 +0000 Subject: [TYPES] ETAPS bars Russian researchers from attending Message-ID: 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 From tringer at cs.washington.edu Tue Mar 8 13:55:33 2022 From: tringer at cs.washington.edu (Talia Ringer) Date: Tue, 8 Mar 2022 12:55:33 -0600 Subject: [TYPES] ETAPS bars Russian researchers from attending In-Reply-To: References: Message-ID: 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 > From alastair.donaldson at imperial.ac.uk Tue Mar 8 14:04:06 2022 From: alastair.donaldson at imperial.ac.uk (Donaldson, Alastair F) Date: Tue, 8 Mar 2022 19:04:06 +0000 Subject: [TYPES] ETAPS bars Russian researchers from attending In-Reply-To: References: Message-ID: I fully agree, Neel and Talia - it's a bad move. While I can see the argument for major corporations denying their services to Russia (e.g. McDonalds closing its restaurants) - because this kind of thing might contribute to the tipping point that's needed for change, applying this to all kinds of minor things starts to feel like Russiaphobia and/or mere virtue signalling. Best wishes Ally ________________________________ From: Types-list on behalf of Talia Ringer Sent: 08 March 2022 18:55 To: Neel Krishnaswami Cc: types-list at lists.seas.upenn.edu Subject: Re: [TYPES] ETAPS bars Russian researchers from attending [ 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 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 > From jung at mpi-sws.org Tue Mar 8 14:04:38 2022 From: jung at mpi-sws.org (Ralf Jung) Date: Tue, 8 Mar 2022 14:04:38 -0500 Subject: [TYPES] ETAPS bars Russian researchers from attending In-Reply-To: References: Message-ID: <42f9065c-2c0b-36cf-c00d-bc8201172d7e@mpi-sws.org> Dear all, I fully agree with you, Neel. The Russian regime started this war, not these researchers. This is the kind of sanction that will primarily hit the wrong people. If financial sanctions make it harder for Russians to attend conferences, we should find ways to support our colleagues -- fostering international collaboration in our community seems more important now than ever. Kind regards, Ralf On 08.03.22 10:01, Neel Krishnaswami 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 From jon at jonmsterling.com Tue Mar 8 14:35:11 2022 From: jon at jonmsterling.com (Jon Sterling) Date: Tue, 08 Mar 2022 20:35:11 +0100 Subject: [TYPES] ETAPS bars Russian researchers from attending In-Reply-To: References: Message-ID: <19608b8c-b629-495e-9f81-529b554a8f19@www.fastmail.com> 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 between those that are "ok" and those that are "not ok". If we were banning researchers participation because their home countries are carrying out imperialist wars or colonization, I would certainly not be allowed to participate in any conferences. Meanwhile, another large conference is being held in a country that I cannot safely enter because of my public stance against colonization. I wonder why this is? We must remember that today, in a world that it ruled by imperialism, the ordinary people are not to blame. We are not the disease, but the cure. Basing participation in scientific discourse on the ruling country of people's employers, or on ideological catechisms, is profoundly wrong and counterproductive. I write with hope that the ETAPS organizers will recognize this as a mistake and change their policy. Best, Jon On Tue, Mar 8, 2022, at 4:01 PM, Neel Krishnaswami 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 From sergyy at gmail.com Tue Mar 8 14:48:50 2022 From: sergyy at gmail.com (Sergey Goncharov) Date: Tue, 8 Mar 2022 20:48:50 +0100 Subject: [TYPES] ETAPS bars Russian researchers from attending In-Reply-To: References: Message-ID: <9127d0b9-80e5-7c9b-3547-eda22be37ca9@gmail.com> Dear Neel, > > 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? > I personally think that you are underestimating the magnitude of the drastic events that are happening. I might be biased, because I come originally from Ukraine and I have to watch now in real time how the places where I lived and which I loved are being demolished cruelly and methodically together with the population without any reason whatsoever. And I feel helpless seeing that I cannot do anything about it. Collective responsibility is always a tricky thing. Normally, you do not want it. Normally. But the present situation is far from normal, far far away from normal. Is it OK to say, well, we are against a nazi regime, but there are many nice people in there, why should we punish them? Maybe they are indeed nice, but they are serving that bloody regime. Nothing personal. They do empower the regime, by their reputation, by making it look more prestigious, making it look "normal" from the inside and the outside, which can, and (I assure you) will be used by propaganda precisely in this way. If there is a chance to send a signal to the effect "it is not normal" in whatever way, I am sorry, but I would do this by any means, without hesitation. And it is not about "nationality", it is about "affiliation". Russians in Europe are "European scientists", Russians in Russia are "Putin's scientists" -- that is how it works mentally. In that sense, the formulation by ETAPS is very correct, in my opinion. Cheers, Sergey From gabriel.scherer at gmail.com Tue Mar 8 15:24:37 2022 From: gabriel.scherer at gmail.com (Gabriel Scherer) Date: Tue, 8 Mar 2022 21:24:37 +0100 Subject: [TYPES] ETAPS bars Russian researchers from attending In-Reply-To: References: Message-ID: Do people know of any precedent of a conference forbidding people working in a certain country to attend? (Of course, on a regular basis we hold conferences in countries that make it difficult for some of our colleagues to attend. But this sounds very different from the conference itself forbidding certain researchers from attending on the basis of their country of employment.) On Tue, Mar 8, 2022 at 7: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 > From marino.miculan at uniud.it Tue Mar 8 16:31:51 2022 From: marino.miculan at uniud.it (Marino Miculan) Date: Tue, 8 Mar 2022 21:31:51 +0000 Subject: [TYPES] R: ETAPS bars Russian researchers from attending In-Reply-To: <9127d0b9-80e5-7c9b-3547-eda22be37ca9@gmail.com> References: <9127d0b9-80e5-7c9b-3547-eda22be37ca9@gmail.com> Message-ID: I agree with Sergey. Maybe some of you have missed the following post from the Russian Rectors' union, fully supporting the invasion of Ukraine. Signed by 185 rectors - I guess, all Russian universities (correct me if I am wrong). https://urldefense.com/v3/__https://www.rsr-online.ru/news/2022-god/obrashchenie-rossiyskogo-soyuza-rektorov1/__;!!IBzWLUs!FxNpRHKpndUzqHVYfL875gRNUF6LDxgWF3Lmq4IGTMUYwYiZDtAZM0erpyfBXgYOogbNe9OTV8A$ Giving space and visibility to research coming from these universities is tantamaunt to admit that these universities (and hence, their researchers, as far as we know) can support war crimes. Of course, I am sure that there are many colleagues there against the invasion. But then, we have to distinguish between the responsibility of the single, and that of the institution. For instance, I would have no problems if a researcher from a Russian university registers and presents their results at ETAPS (or any other conference) without? any affiliation. That would be already a strong signal, as in "I'm here on my own, and I dissociate from my rector's opinions". best -marino ________________________________ Da: Types-list per conto di Sergey Goncharov Inviato: marted? 8 marzo 2022 20:48 A: Neel Krishnaswami ; types-list at lists.seas.upenn.edu Oggetto: Re: [TYPES] ETAPS bars Russian researchers from attending [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] Dear Neel, > > 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? > I personally think that you are underestimating the magnitude of the drastic events that are happening. I might be biased, because I come originally from Ukraine and I have to watch now in real time how the places where I lived and which I loved are being demolished cruelly and methodically together with the population without any reason whatsoever. And I feel helpless seeing that I cannot do anything about it. Collective responsibility is always a tricky thing. Normally, you do not want it. Normally. But the present situation is far from normal, far far away from normal. Is it OK to say, well, we are against a nazi regime, but there are many nice people in there, why should we punish them? Maybe they are indeed nice, but they are serving that bloody regime. Nothing personal. They do empower the regime, by their reputation, by making it look more prestigious, making it look "normal" from the inside and the outside, which can, and (I assure you) will be used by propaganda precisely in this way. If there is a chance to send a signal to the effect "it is not normal" in whatever way, I am sorry, but I would do this by any means, without hesitation. And it is not about "nationality", it is about "affiliation". Russians in Europe are "European scientists", Russians in Russia are "Putin's scientists" -- that is how it works mentally. In that sense, the formulation by ETAPS is very correct, in my opinion. Cheers, Sergey From ricardo.h.medel at gmail.com Tue Mar 8 18:29:10 2022 From: ricardo.h.medel at gmail.com (Ricardo Medel) Date: Tue, 8 Mar 2022 20:29:10 -0300 Subject: [TYPES] ETAPS bars Russian researchers from attending In-Reply-To: References: Message-ID: German scientists were banned from conferences after the First World War. Chinese scientists (even those working/studying at the USA) were banned from attending a NASA conference in 2013. El mar., 8 de marzo de 2022 17:25, Gabriel Scherer < gabriel.scherer at gmail.com> escribi?: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > Do people know of any precedent of a conference forbidding people working > in a certain country to attend? > > (Of course, on a regular basis we hold conferences in countries that make > it difficult for some of our colleagues to attend. But this sounds very > different from the conference itself forbidding certain researchers from > attending on the basis of their country of employment.) > > > On Tue, Mar 8, 2022 at 7: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 > > > From anas at cs.uni-salzburg.at Wed Mar 9 01:42:18 2022 From: anas at cs.uni-salzburg.at (Ana Sokolova) Date: Wed, 9 Mar 2022 07:42:18 +0100 Subject: [TYPES] Types-list Digest, Vol 140, Issue 1 In-Reply-To: References: Message-ID: 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 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 > 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 > To: Julin S > Cc: Types list > 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 > To: types-list at lists.seas.upenn.edu > Subject: [TYPES] Consistency of NF > Message-ID: > 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 > To: types-list at lists.seas.upenn.edu > Subject: [TYPES] ETAPS bars Russian researchers from attending > Message-ID: > 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 > To: Neel Krishnaswami > 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 > ****************************************** > From julinshaji01 at gmail.com Wed Mar 9 03:54:23 2022 From: julinshaji01 at gmail.com (Julin S) Date: Wed, 9 Mar 2022 14:24:23 +0530 Subject: [TYPES] R: ETAPS bars Russian researchers from attending In-Reply-To: References: <9127d0b9-80e5-7c9b-3547-eda22be37ca9@gmail.com> Message-ID: I feel that it's very wrong and will lead to serious adverse consequences on the whole scientific community if individuals ostracized based on their country. Let's not contribute to the fragmentation the academic community. Mixing academics with political decisions of governments (and not of the people being governed by them), is a very bad idea. I suppose it's already been mentioned implcitly, but let us not forget that people can also be forced into signing things. On Wed, Mar 9, 2022 at 1:33 PM Marino Miculan wrote: > > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > I agree with Sergey. Maybe some of you have missed the following post from the Russian Rectors' union, fully supporting the invasion of Ukraine. Signed by 185 rectors - I guess, all Russian universities (correct me if I am wrong). > > https://urldefense.com/v3/__https://www.rsr-online.ru/news/2022-god/obrashchenie-rossiyskogo-soyuza-rektorov1/__;!!IBzWLUs!FxNpRHKpndUzqHVYfL875gRNUF6LDxgWF3Lmq4IGTMUYwYiZDtAZM0erpyfBXgYOogbNe9OTV8A$ > > Giving space and visibility to research coming from these universities is tantamaunt to admit that these universities (and hence, their researchers, as far as we know) can support war crimes. From alejandro at diaz-caro.info Wed Mar 9 04:41:22 2022 From: alejandro at diaz-caro.info (=?UTF-8?Q?Alejandro_D=C3=ADaz=2DCaro?=) Date: Wed, 9 Mar 2022 06:41:22 -0300 Subject: [TYPES] R: ETAPS bars Russian researchers from attending In-Reply-To: References: <9127d0b9-80e5-7c9b-3547-eda22be37ca9@gmail.com> Message-ID: Dear Marino, dear all, El mi?, 9 mar. 2022 05:05, Marino Miculan escribi?: > > Of course, I am sure that there are many colleagues there against the > invasion. But then, we have to distinguish between the responsibility of > the single, and that of the institution. For instance, I would have no > problems if a researcher from a Russian university registers and presents > their results at ETAPS (or any other conference) without? any affiliation. > That would be already a strong signal, as in "I'm here on my own, and I > dissociate from my rector's opinions". > That would be even worst than the decision of banning a country by their war politics. What you are proposing there is to ask the researchers about their political personal opinion in order to be admitted to a conference. I find this completely wrong. Shall we also inquire Cubans if they support Fidel Castro or Americans if they support the blockade? Shall we ask Israel or Palestinians what side of the conflict they support, and let them register according to the personal stand of the organisers at the venue? I think that mixing politics with the scientific community at this global level is very dangerous and ultimately wrong. I hope this line of actions do not prosper, or we will damage the scientific community for many years. Best, Alejandro > From wadler at inf.ed.ac.uk Wed Mar 9 06:44:36 2022 From: wadler at inf.ed.ac.uk (Philip Wadler) Date: Wed, 9 Mar 2022 08:44:36 -0300 Subject: [TYPES] ETAPS bars Russian researchers from attending In-Reply-To: References: Message-ID: To add to Ricardo's examples, during Apartheid, there was an academic boycott of South Africa as part of a larger cultural boycott, similar to the cultural boycott of Russia we see beginning today. This included not accepting academic visitors affiliated with South Africa, even though many South African academics opposed Apartheid. Treating Russian institutions differently at this time can contribute to a cumulative effect. Failing to treat them differently sends the message that we don't care. Go well, -- P . \ Philip Wadler, Professor of Theoretical Computer Science, . /\ School of Informatics, University of Edinburgh . / \ and Senior Research Fellow, IOHK . https://urldefense.com/v3/__http://homepages.inf.ed.ac.uk/wadler/__;!!IBzWLUs!ByhpRFSKZ3IGEazSYRk8ZiPNOU_tVRrh8Q_83QpOs_9HzrHFz55B0xkCfLYICuE4ayzyajgRdTs$ On Tue, 8 Mar 2022 at 20:29, Ricardo Medel wrote: > This email was sent to you by someone outside the University. > You should only click on links or attachments if you are certain that the > email is genuine and the content is safe. > > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > German scientists were banned from conferences after the First World War. > > Chinese scientists (even those working/studying at the USA) were banned > from attending a NASA conference in 2013. > > > > > El mar., 8 de marzo de 2022 17:25, Gabriel Scherer < > gabriel.scherer at gmail.com> escribi?: > > > [ The Types Forum, > http://lists.seas.upenn.edu/mailman/listinfo/types-list > > ] > > > > Do people know of any precedent of a conference forbidding people working > > in a certain country to attend? > > > > (Of course, on a regular basis we hold conferences in countries that make > > it difficult for some of our colleagues to attend. But this sounds very > > different from the conference itself forbidding certain researchers from > > attending on the basis of their country of employment.) > > > > > > On Tue, Mar 8, 2022 at 7: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 > > > > > > -------------- next part -------------- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. From bogom.s at gmail.com Wed Mar 9 05:43:27 2022 From: bogom.s at gmail.com (Sergiy Bogomolov) Date: Wed, 9 Mar 2022 10:43:27 +0000 Subject: [TYPES] R: ETAPS bars Russian researchers from attending In-Reply-To: References: <9127d0b9-80e5-7c9b-3547-eda22be37ca9@gmail.com> Message-ID: Let me start by saying that I strongly support the ETAPS decision to ban the participation of Russian affiliated scientists at the conference. The rationale is the as follows: * The ongoing war in Ukraine is at least partially due to the weak response of the Western countries to the Russian invasion of Ukraine in 2014 and Georgia in 2008. In fact, the Western countries introduced very targeted sanctions which, e.g., banned some Russian officials from entering the US (which they did not care about anyway). At the same time -- exactly in line with the arguments proposed by the folks who want to overturn the decision of ETAPS organisers -- the broad Russian population did not bear the burden of the sanctions. Have these sanctions helped? No, they have not. In fact, these only reassured the Russian regime that the West is "weak" and they can go ahead with a fully-fledged war in Ukraine without fearing any implications. In other words, all the efforts to change the course of actions of the Russian government without negatively impacting the Russian population have failed. * At the same time, upon the commencement of the war in Ukraine, the Western governments seem to have learnt the lesson and have devised the sanction regime which should hurt the Russian population as a whole and make them finally give some thoughts about the decisions of their government and the fact that these might be in fact counterproductive to their prosperity. This is an unfortunate reality that the West has to resolve to this kind of approach, but I believe there are only a limited number of ways to stop the war without ending up in a direct military confrontation between the West and Russia. * To everybody who suggests overturning the decision of ETAPS organisers I suggest the following thought experiment. Imagine you go to bed without knowing you are going to be alive in the morning (as Russian army pursues indiscriminate bombing of residential areas; including the city of Kharkiv where I grew up). Imagine getting up in the morning and calling your relatives to check out whether they are still alive. If you were in such a situation, would you still be willing to allow the Russian affiliated scientists to participate in the conference? This is the reality myself and all the Ukrainians are living through. Now, consider whether prohibiting the participation of Russian affiliated scientists -- who did not participate at ETAPS en masse anyway -- which could bring the end of war a step closer outweighs the arguments to let the Russian affiliated scientists participate in the conference. Thanks, Sergiy On Wed, 9 Mar 2022 at 09:50, Alejandro D?az-Caro wrote: > > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Dear Marino, dear all, > > El mi?, 9 mar. 2022 05:05, Marino Miculan > escribi?: > > > > > Of course, I am sure that there are many colleagues there against the > > invasion. But then, we have to distinguish between the responsibility of > > the single, and that of the institution. For instance, I would have no > > problems if a researcher from a Russian university registers and presents > > their results at ETAPS (or any other conference) without any affiliation. > > That would be already a strong signal, as in "I'm here on my own, and I > > dissociate from my rector's opinions". > > > > That would be even worst than the decision of banning a country by their > war politics. What you are proposing there is to ask the researchers about > their political personal opinion in order to be admitted to a conference. I > find this completely wrong. > > Shall we also inquire Cubans if they support Fidel Castro or Americans if > they support the blockade? Shall we ask Israel or Palestinians what side of > the conflict they support, and let them register according to the personal > stand of the organisers at the venue? > > I think that mixing politics with the scientific community at this global > level is very dangerous and ultimately wrong. > > I hope this line of actions do not prosper, or we will damage the > scientific community for many years. > > Best, > Alejandro > > > From gabriel.scherer at gmail.com Wed Mar 9 07:25:22 2022 From: gabriel.scherer at gmail.com (Gabriel Scherer) Date: Wed, 9 Mar 2022 13:25:22 +0100 Subject: [TYPES] ETAPS bars Russian researchers from attending In-Reply-To: References: Message-ID: I looked for more sources on the examples of Ricardo and Phil. - The 2013 NASA event is described in the following press articles: https://urldefense.com/v3/__https://edition.cnn.com/2013/10/20/world/asia/china-nasa-drama/index.html__;!!IBzWLUs!GhQK6_S6GyjP-V9HmwwzBik-u6R4jdNiLP2q_jATNCsbxUdf3BvEwf5qgsfCz89kEoDJu8D9Itc$ https://urldefense.com/v3/__https://www.theguardian.com/science/2013/oct/11/nasa-chinese-scientists-conference-ban__;!!IBzWLUs!GhQK6_S6GyjP-V9HmwwzBik-u6R4jdNiLP2q_jATNCsbxUdf3BvEwf5qgsfCz89kEoDJ58lVgdI$ It is not clear from the articles what the real motivation for the ban was, but the justification was internal regulations in the US at the time. The ban was apparently reversed before the conference took place, after a large public outcry. The decision was made by NASA -- the conference was hosted within a NASA facility. (This is not a computer science conference.) - There is a wikipedia page on the academic boycott of South Africa: https://urldefense.com/v3/__https://en.wikipedia.org/wiki/Academic_boycott_of_South_Africa__;!!IBzWLUs!GhQK6_S6GyjP-V9HmwwzBik-u6R4jdNiLP2q_jATNCsbxUdf3BvEwf5qgsfCz89kEoDJ90qzEyk$ It details that this was a controversial topic at the time outside the country, even in anti-apartheid groups. On Wed, Mar 9, 2022 at 12:45 PM Philip Wadler wrote: > To add to Ricardo's examples, during Apartheid, there was an academic > boycott of South Africa as part of a larger cultural boycott, similar to > the cultural boycott of Russia we see beginning today. This included not > accepting academic visitors affiliated with South Africa, even though many > South African academics opposed Apartheid. Treating Russian institutions > differently at this time can contribute to a cumulative effect. Failing to > treat them differently sends the message that we don't care. Go well, -- P > > > . \ Philip Wadler, Professor of Theoretical Computer Science, > . /\ School of Informatics, University of Edinburgh > . / \ and Senior Research Fellow, IOHK > . https://urldefense.com/v3/__http://homepages.inf.ed.ac.uk/wadler/__;!!IBzWLUs!GhQK6_S6GyjP-V9HmwwzBik-u6R4jdNiLP2q_jATNCsbxUdf3BvEwf5qgsfCz89kEoDJyX679Vo$ > > > > On Tue, 8 Mar 2022 at 20:29, Ricardo Medel > wrote: > >> This email was sent to you by someone outside the University. >> You should only click on links or attachments if you are certain that the >> email is genuine and the content is safe. >> >> [ The Types Forum, >> http://lists.seas.upenn.edu/mailman/listinfo/types-list ] >> >> German scientists were banned from conferences after the First World War. >> >> Chinese scientists (even those working/studying at the USA) were banned >> from attending a NASA conference in 2013. >> >> >> >> >> El mar., 8 de marzo de 2022 17:25, Gabriel Scherer < >> gabriel.scherer at gmail.com> escribi?: >> >> > [ The Types Forum, >> http://lists.seas.upenn.edu/mailman/listinfo/types-list >> > ] >> > >> > Do people know of any precedent of a conference forbidding people >> working >> > in a certain country to attend? >> > >> > (Of course, on a regular basis we hold conferences in countries that >> make >> > it difficult for some of our colleagues to attend. But this sounds very >> > different from the conference itself forbidding certain researchers from >> > attending on the basis of their country of employment.) >> > >> > >> > On Tue, Mar 8, 2022 at 7: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 >> > > >> > >> > The University of Edinburgh is a charitable body, registered in > Scotland, with registration number SC005336. > From julbinb at gmail.com Wed Mar 9 07:59:16 2022 From: julbinb at gmail.com (Julia Belyakova) Date: Wed, 9 Mar 2022 07:59:16 -0500 Subject: [TYPES] R: ETAPS bars Russian researchers from attending In-Reply-To: References: <9127d0b9-80e5-7c9b-3547-eda22be37ca9@gmail.com> Message-ID: Just FYI about rectors' letters: most Russian universities are state universities, and in many of them, rectors are literally government appointees, not elected by the university body. There were various independent antiwar letters signed by academics, including people working in the institutions whose rectors signed the pro-Putin letters. The university admins don't represent the scientific community. -- Kind regards, Julia On Wed, Mar 9, 2022, 04:30 Marino Miculan wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > I agree with Sergey. Maybe some of you have missed the following post > from the Russian Rectors' union, fully supporting the invasion of Ukraine. > Signed by 185 rectors - I guess, all Russian universities (correct me if I > am wrong). > > > https://urldefense.com/v3/__https://www.rsr-online.ru/news/2022-god/obrashchenie-rossiyskogo-soyuza-rektorov1/__;!!IBzWLUs!FxNpRHKpndUzqHVYfL875gRNUF6LDxgWF3Lmq4IGTMUYwYiZDtAZM0erpyfBXgYOogbNe9OTV8A$ > > Giving space and visibility to research coming from these universities is > tantamaunt to admit that these universities (and hence, their researchers, > as far as we know) can support war crimes. > > Of course, I am sure that there are many colleagues there against the > invasion. But then, we have to distinguish between the responsibility of > the single, and that of the institution. For instance, I would have no > problems if a researcher from a Russian university registers and presents > their results at ETAPS (or any other conference) without? any affiliation. > That would be already a strong signal, as in "I'm here on my own, and I > dissociate from my rector's opinions". > > best > -marino > > > ________________________________ > Da: Types-list per conto di > Sergey Goncharov > Inviato: marted? 8 marzo 2022 20:48 > A: Neel Krishnaswami ; > types-list at lists.seas.upenn.edu > Oggetto: Re: [TYPES] ETAPS bars Russian researchers from attending > > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > Dear Neel, > > > > > 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? > > > > I personally think that you are underestimating the magnitude of the > drastic events that are happening. > I might be biased, because I come originally from Ukraine and I have to > watch now in real time how the > places where I lived and which I loved are being demolished cruelly and > methodically together with the > population without any reason whatsoever. And I feel helpless seeing that > I cannot do anything about it. > > Collective responsibility is always a tricky thing. Normally, you do not > want it. Normally. But the > present situation is far from normal, far far away from normal. > > Is it OK to say, well, we are against a nazi regime, but there are many > nice people in there, why should > we punish them? Maybe they are indeed nice, but they are serving that > bloody regime. Nothing personal. > They do empower the regime, by their reputation, by making it look more > prestigious, making it look > "normal" from the inside and the outside, which can, and (I assure you) > will be used by propaganda > precisely in this way. If there is a chance to send a signal to the effect > "it is not normal" in > whatever way, I am sorry, but I would do this by any means, without > hesitation. > > And it is not about "nationality", it is about "affiliation". Russians in > Europe are "European > scientists", Russians in Russia are "Putin's scientists" -- that is how it > works mentally. In that > sense, the formulation by ETAPS is very correct, in my opinion. > > Cheers, > Sergey > > From gabriel.scherer at gmail.com Wed Mar 9 08:53:42 2022 From: gabriel.scherer at gmail.com (Gabriel Scherer) Date: Wed, 9 Mar 2022 14:53:42 +0100 Subject: [TYPES] ETAPS bars Russian researchers from attending In-Reply-To: References: Message-ID: I find this decision by ETAPS shocking. I was considering attending ETAPS 2022, and I will not go. I view scientific research as a universal pursuit of knowledge in the benefit of humankind. We are funded by nations, but we work together on a shared goal. (This is not just me, this is also a definition used by UNESCO.) Preventing scientific researchers from attending a scientific event runs counter to that goal, and is a clear limitation of academic freedom. I don't think that ETAPS can justify its decision according to those principles. I don't know how this decision, which concerns the whole scientific community (not just ETAPS board members) has been taken, and I don't see any detailed justification of it publicly available. Limiting participation in scientific activities is a grave decision that should be justified carefully, announced well in advance, and provide clear avenues for affected people to understand how to regain their ability to participate. I don't see any such justification and processes here. In these difficult times I find it useful to look for external confirmations that my view of research matches other peoples' reality as well. Please find at the end of this email some relevant excerpts from UNESCO texts that I happened to find easily. Preventing people from participating in academic conferences is not an economic sanction, it is not comparable to McDonalds stopping business in Russia. We should also be careful about comparisons with sports: international sports are a *competition*, while international research is mostly collaborative -- with competitive aspects as well. (I wasn't aware of the precedent in South Africa which I find very interesting. But I still find it a fairly different situation: South African scientists were living in an Apartheid society for years, whereas we are talking of an unprovoked war that is less than a month old. We should also absolutely avoid trying to make decision on the publicly perceived opinions/support of our colleagues working in Russia -- they live in a country where spreading "misinformation about the special operations" can send you to jail.) Of course, working for all of humankind is one aspect of international research, but there are also aspects of our work that advance national or regional interests. I understand the argument that institutional affiliations are a form of soft power, and that they are, in small part, empowering our institutions and nations. ETAPS could have decided to disallow researchers from indicating a Russian affiliation (or even to not track affiliations at all, for everyone, in support of global peace and as a reference to our universal values). As far as I know, this would not have run afoul of the general principles of equal access to science and academic freedom. None of this should be taken as a minimization of the immense pain caused by the tragedy going on in Ukraine right now due to Russia's unprovoked war. I'm sure that ETAPS could find ways to indicate their support of the Ukrainian people, and all people affected by this war. Here in France we have a national initiative (the PAUSE programme run by Coll?ge de France : https://urldefense.com/v3/__https://www.college-de-france.fr/site/en-program-pause/Presentation-of-the-program.htm__;!!IBzWLUs!Faih7fEiuqHGj0gHXJugoZ0DWjGZpLM1D8VQmRhhPdjNUplx_k2OlPAWYIyuqC-qxiZXde6S0h4$ ) to host scientists and artists in exile. Our hierarchy signalled that funding would be available for people displaced by the war in Ukraine; if you are concerned and would like to come work in France, please get in touch with colleagues working in French institutions. (The institutions hire the displaced scientists, funded by the programme.) ---- Paragraph 31 of the UNESCO 2018 document "Recommendation on science and scientific researchers" states: Member States should actively promote the interplay of > ideas and information among scientific researchers throughout the world, > which is > vital to the healthy development of the sciences; and to this end, should > take all > measures necessary to ensure that scientific researchers are enabled, > throughout > their careers, to participate in international scientific and > technological community. > Member States should facilitate this travel in and out of their territory. > Paragraph 14.b of the 2021 Unesco Recommendation on Open Science states: Equality of opportunities: all scientists and other open science > actors and stakeholders, regardless of location, nationality, race, > age, gender, income, socio-economic circumstances, career stage, > discipline, language, religion, disability, ethnicity or migratory status, > or any other grounds, have an equal opportunity to access, and > contribute to and benefit from open science. Paragraph 27 of the 1997 UNESCO statement on Academic Freedom includes: The maintaining of the above international standards should be > upheld in the interest of higher education internationally and > within the country. [...] Higher-education teaching > personnel are entitled to the maintaining of academic freedom, > that is to say, the right, without constriction by prescribed > doctrine, to freedom of teaching and discussion, freedom in > carrying out research and disseminating and publishing the > results thereof, freedom to express freely their opinion about > the institution or system in which they work, freedom from > institutional censorship and freedom to participate in > professional or representative academic bodies. All > higher-education teaching personnel should have the right to > fulfil their functions without discrimination of any kind and > without fear of repression by the state or any other source. > To me it is clear that banning researchers from attending conferences based on their location of employment violates these principles. On Tue, Mar 8, 2022 at 7: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 > From bogom.s at gmail.com Wed Mar 9 07:43:39 2022 From: bogom.s at gmail.com (Sergiy Bogomolov) Date: Wed, 9 Mar 2022 12:43:39 +0000 Subject: [TYPES] R: ETAPS bars Russian researchers from attending In-Reply-To: References: <9127d0b9-80e5-7c9b-3547-eda22be37ca9@gmail.com> Message-ID: > Banning scientists from ETAPS won't do anything to bring the end of war a step closer. > Banning Netflix, McDonalds, Visa, Mastercard, etc., etc., from Russia, and ceasing to purchase fossil fuels from Russia might. Banning scientific conferences won't have any impact. Alastair: Thanks for your comment. I am afraid I don't really agree with this statement. At this stage, the whole essence of large-scale sanctions is to inflict pain on the Russian population, with the aim to reduce their support of the Putin regime. In this context, the larger part of the population is targeted, the more impact sanctions are going to have. Russian researchers are part of the whole population and one of the ways to hit them is to prohibit their participation in international conferences. In other words, I see the step of ETAPS organisers -- similar to banning Netflix, etc. -- as yet another tool to target a particular demographic, which the West should deploy to stop the war. I hope this makes sense. Thanks, Sergiy > > Cheers > > Ally > > ________________________________ > From: Types-list on behalf of Sergiy Bogomolov > Sent: 09 March 2022 10:43 > To: types > Subject: Re: [TYPES] R: ETAPS bars Russian researchers from attending > > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Let me start by saying that I strongly support the ETAPS decision to > ban the participation of Russian affiliated scientists at the > conference. > > The rationale is the as follows: > > * The ongoing war in Ukraine is at least partially due to the weak > response of the Western countries to the Russian invasion of Ukraine > in 2014 and Georgia in 2008. In fact, the Western countries introduced > very targeted sanctions which, e.g., banned some Russian officials > from entering the US (which they did not care about anyway). At the > same time -- exactly in line with the arguments proposed by the folks > who want to overturn the decision of ETAPS organisers -- the broad > Russian population did not bear the burden of the sanctions. Have > these sanctions helped? No, they have not. In fact, these only > reassured the Russian regime that the West is "weak" and they can go > ahead with a fully-fledged war in Ukraine without fearing any > implications. In other words, all the efforts to change the course of > actions of the Russian government without negatively impacting the > Russian population have failed. > > * At the same time, upon the commencement of the war in Ukraine, the > Western governments seem to have learnt the lesson and have devised > the sanction regime which should hurt the Russian population as a > whole and make them finally give some thoughts about the decisions of > their government and the fact that these might be in fact > counterproductive to their prosperity. This is an unfortunate reality > that the West has to resolve to this kind of approach, but I believe > there are only a limited number of ways to stop the war without ending > up in a direct military confrontation between the West and Russia. > > * To everybody who suggests overturning the decision of ETAPS > organisers I suggest the following thought experiment. Imagine you go > to bed without knowing you are going to be alive in the morning (as > Russian army pursues indiscriminate bombing of residential areas; > including the city of Kharkiv where I grew up). Imagine getting up in > the morning and calling your relatives to check out whether they are > still alive. If you were in such a situation, would you still be > willing to allow the Russian affiliated scientists to participate in > the conference? This is the reality myself and all the Ukrainians are > living through. Now, consider whether prohibiting the participation of > Russian affiliated scientists -- who did not participate at ETAPS en > masse anyway -- which could bring the end of war a step closer > outweighs the arguments to let the Russian affiliated scientists > participate in the conference. > > Thanks, Sergiy > > > > > > On Wed, 9 Mar 2022 at 09:50, Alejandro D?az-Caro > wrote: > > > > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > > > Dear Marino, dear all, > > > > El mi?, 9 mar. 2022 05:05, Marino Miculan > > escribi?: > > > > > > > > Of course, I am sure that there are many colleagues there against the > > > invasion. But then, we have to distinguish between the responsibility of > > > the single, and that of the institution. For instance, I would have no > > > problems if a researcher from a Russian university registers and presents > > > their results at ETAPS (or any other conference) without any affiliation. > > > That would be already a strong signal, as in "I'm here on my own, and I > > > dissociate from my rector's opinions". > > > > > > > That would be even worst than the decision of banning a country by their > > war politics. What you are proposing there is to ask the researchers about > > their political personal opinion in order to be admitted to a conference. I > > find this completely wrong. > > > > Shall we also inquire Cubans if they support Fidel Castro or Americans if > > they support the blockade? Shall we ask Israel or Palestinians what side of > > the conflict they support, and let them register according to the personal > > stand of the organisers at the venue? > > > > I think that mixing politics with the scientific community at this global > > level is very dangerous and ultimately wrong. > > > > I hope this line of actions do not prosper, or we will damage the > > scientific community for many years. > > > > Best, > > Alejandro > > > > > From maxsnew at gmail.com Wed Mar 9 10:27:45 2022 From: maxsnew at gmail.com (Max New) Date: Wed, 9 Mar 2022 10:27:45 -0500 Subject: [TYPES] R: ETAPS bars Russian researchers from attending In-Reply-To: References: <9127d0b9-80e5-7c9b-3547-eda22be37ca9@gmail.com> Message-ID: ETAPS has rescinded this policy as of today. The statement on the website is as follows now: 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. For more information, please refer to the Statement of Alliance of Science Organisations in Germany . -Max Stewart New On Wed, Mar 9, 2022 at 9:05 AM Sergiy Bogomolov wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > > Banning scientists from ETAPS won't do anything to bring the end of war > a step closer. > > Banning Netflix, McDonalds, Visa, Mastercard, etc., etc., from Russia, > and ceasing to purchase fossil fuels from Russia might. Banning scientific > conferences won't have any impact. > > Alastair: Thanks for your comment. I am afraid I don't really agree > with this statement. > > At this stage, the whole essence of large-scale sanctions is to > inflict pain on the Russian population, with the aim to reduce their > support of the Putin regime. > > In this context, the larger part of the population is targeted, the > more impact sanctions are going to have. > > Russian researchers are part of the whole population and one of the > ways to hit them is to prohibit their participation in international > conferences. > > In other words, I see the step of ETAPS organisers -- similar to > banning Netflix, etc. -- as yet another tool to target a particular > demographic, which the West should deploy to stop the war. > > I hope this makes sense. > > Thanks, Sergiy > > > > > > Cheers > > > > Ally > > > > ________________________________ > > From: Types-list on behalf of > Sergiy Bogomolov > > Sent: 09 March 2022 10:43 > > To: types > > Subject: Re: [TYPES] R: ETAPS bars Russian researchers from attending > > > > [ The Types Forum, > http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > > > Let me start by saying that I strongly support the ETAPS decision to > > ban the participation of Russian affiliated scientists at the > > conference. > > > > The rationale is the as follows: > > > > * The ongoing war in Ukraine is at least partially due to the weak > > response of the Western countries to the Russian invasion of Ukraine > > in 2014 and Georgia in 2008. In fact, the Western countries introduced > > very targeted sanctions which, e.g., banned some Russian officials > > from entering the US (which they did not care about anyway). At the > > same time -- exactly in line with the arguments proposed by the folks > > who want to overturn the decision of ETAPS organisers -- the broad > > Russian population did not bear the burden of the sanctions. Have > > these sanctions helped? No, they have not. In fact, these only > > reassured the Russian regime that the West is "weak" and they can go > > ahead with a fully-fledged war in Ukraine without fearing any > > implications. In other words, all the efforts to change the course of > > actions of the Russian government without negatively impacting the > > Russian population have failed. > > > > * At the same time, upon the commencement of the war in Ukraine, the > > Western governments seem to have learnt the lesson and have devised > > the sanction regime which should hurt the Russian population as a > > whole and make them finally give some thoughts about the decisions of > > their government and the fact that these might be in fact > > counterproductive to their prosperity. This is an unfortunate reality > > that the West has to resolve to this kind of approach, but I believe > > there are only a limited number of ways to stop the war without ending > > up in a direct military confrontation between the West and Russia. > > > > * To everybody who suggests overturning the decision of ETAPS > > organisers I suggest the following thought experiment. Imagine you go > > to bed without knowing you are going to be alive in the morning (as > > Russian army pursues indiscriminate bombing of residential areas; > > including the city of Kharkiv where I grew up). Imagine getting up in > > the morning and calling your relatives to check out whether they are > > still alive. If you were in such a situation, would you still be > > willing to allow the Russian affiliated scientists to participate in > > the conference? This is the reality myself and all the Ukrainians are > > living through. Now, consider whether prohibiting the participation of > > Russian affiliated scientists -- who did not participate at ETAPS en > > masse anyway -- which could bring the end of war a step closer > > outweighs the arguments to let the Russian affiliated scientists > > participate in the conference. > > > > Thanks, Sergiy > > > > > > > > > > > > On Wed, 9 Mar 2022 at 09:50, Alejandro D?az-Caro > > wrote: > > > > > > [ The Types Forum, > http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > > > > > Dear Marino, dear all, > > > > > > El mi?, 9 mar. 2022 05:05, Marino Miculan > > > escribi?: > > > > > > > > > > > Of course, I am sure that there are many colleagues there against the > > > > invasion. But then, we have to distinguish between the > responsibility of > > > > the single, and that of the institution. For instance, I would have > no > > > > problems if a researcher from a Russian university registers and > presents > > > > their results at ETAPS (or any other conference) without any > affiliation. > > > > That would be already a strong signal, as in "I'm here on my own, > and I > > > > dissociate from my rector's opinions". > > > > > > > > > > That would be even worst than the decision of banning a country by > their > > > war politics. What you are proposing there is to ask the researchers > about > > > their political personal opinion in order to be admitted to a > conference. I > > > find this completely wrong. > > > > > > Shall we also inquire Cubans if they support Fidel Castro or Americans > if > > > they support the blockade? Shall we ask Israel or Palestinians what > side of > > > the conflict they support, and let them register according to the > personal > > > stand of the organisers at the venue? > > > > > > I think that mixing politics with the scientific community at this > global > > > level is very dangerous and ultimately wrong. > > > > > > I hope this line of actions do not prosper, or we will damage the > > > scientific community for many years. > > > > > > Best, > > > Alejandro > > > > > > > > From jonathan.aldrich at cs.cmu.edu Wed Mar 9 10:36:53 2022 From: jonathan.aldrich at cs.cmu.edu (Jonathan Aldrich) Date: Wed, 9 Mar 2022 10:36:53 -0500 Subject: [TYPES] ETAPS bars Russian researchers from attending In-Reply-To: References: Message-ID: It appears that ETAPS has taken down this policy, along with a related statement that was formerly on the Programme page: "By virtue of participating at ETAPS'22, each participating scientist explicitly condemns the war against Ukraine launched by President Putin as an intolerable breach of international law and a crime against humanity" (was from https://urldefense.com/v3/__https://etaps.org/2022/programme__;!!IBzWLUs!EpsQrWS31b30n9gaZtvqxq7Rq-6qqTlzJ-NVbzT5ftsROBWUU7cwfDXCOxA7gPC83gw-BfS8N2w$ ). This statement was arguably even more problematic, as it is a kind of forced speech, and thus incompatible with academic freedom. It appears both have been replaced with a statement by the organizers, which--while it could still be viewed as bringing ETAPS into politics--seems much less problematic. I thank ETAPS for listening to community concerns here. And, I echo the ETAPS organizers in condemning the invasion of Ukraine and the atrocities that have been committed as part of it. I support the government sanctions against Russia (which also affect attendance at ETAPS), even if I agree with what Neel, Talia, and others say about academic boycotts. Best, Jonathan On Tue, Mar 8, 2022 at 1: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 > From julbinb at gmail.com Wed Mar 9 10:38:14 2022 From: julbinb at gmail.com (Julia Belyakova) Date: Wed, 9 Mar 2022 10:38:14 -0500 Subject: [TYPES] R: ETAPS bars Russian researchers from attending In-Reply-To: References: <9127d0b9-80e5-7c9b-3547-eda22be37ca9@gmail.com> Message-ID: Thank you all for the comments and thoughtful discussion. Being a Russian citizen, I don't feel entitled to argue on the ETAPS decision, and emotionally, I understand the arguments in favor of that decision. I also acknowledge the argument about total isolation of the population potentially sending the right message to the population: > At this stage, the whole essence of large-scale sanctions is to > inflict pain on the Russian population, with the aim to reduce their > support of the Putin regime. > > In this context, the larger part of the population is targeted, the > more impact sanctions are going to have. > > Russian researchers are part of the whole population and one of the > ways to hit them is to prohibit their participation in international > conferences. However, not all the means help the cause. I would like to emphasize that there are a lot of people in Russia who do not and have not supported Putin and the ongoing terrible war in Ukraine. I think it is not unreasonable to assume that the Russian scientific community, especially those who used to attend international conferences and mingle with the international community, are the ones who are most likely to already be in opposition to Putin. Therefore, I do not see how targeting the population that does not support Putin can help with the goal of reducing Putin's support. Isolation can also make it harder for people to find sources of information and see the real picture, playing into Putin's propaganda about the entire world hating Russia. Several days ago, the few remaining independent media have been blocked or forced to stop writing about the war; Twitter and Facebook have been blocked, too, and other platforms are probably going to be blocked soon as well. Note that Russia is not a democratic country. Normal processes such as voting against the regime in an election have not been properly operating there for years. Official numbers of overwhelming Putin's support should be taken with a sack of salt. Since last week, people spreading "misinformation" and "discrediting" the Russian army can face up to 15 years in prison. There haven't been 15-years convictions yet, but the new law is already working, the first sentences have been issued, a number of anti-war protesters have been beaten and tortured by the police, the first students have been expelled from universities for anti-war protests and posts. Opposing the regime had not been easy even before the new law, and if you are interested, I think this thread captures the situation accurately. None of this, of course, compares or lessens the suffering of Ukrainian people in any way. I am devastated and ashamed by Putin's government invasion. The war is unforgivable. Putin has to be stopped. -- Kind regards, Julia On Wed, Mar 9, 2022 at 9:06 AM Sergiy Bogomolov wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > > Banning scientists from ETAPS won't do anything to bring the end of war > a step closer. > > Banning Netflix, McDonalds, Visa, Mastercard, etc., etc., from Russia, > and ceasing to purchase fossil fuels from Russia might. Banning scientific > conferences won't have any impact. > > Alastair: Thanks for your comment. I am afraid I don't really agree > with this statement. > > At this stage, the whole essence of large-scale sanctions is to > inflict pain on the Russian population, with the aim to reduce their > support of the Putin regime. > > In this context, the larger part of the population is targeted, the > more impact sanctions are going to have. > > Russian researchers are part of the whole population and one of the > ways to hit them is to prohibit their participation in international > conferences. > > In other words, I see the step of ETAPS organisers -- similar to > banning Netflix, etc. -- as yet another tool to target a particular > demographic, which the West should deploy to stop the war. > > I hope this makes sense. > > Thanks, Sergiy > > > > > > Cheers > > > > Ally > > > > ________________________________ > > From: Types-list on behalf of > Sergiy Bogomolov > > Sent: 09 March 2022 10:43 > > To: types > > Subject: Re: [TYPES] R: ETAPS bars Russian researchers from attending > > > > [ The Types Forum, > http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > > > Let me start by saying that I strongly support the ETAPS decision to > > ban the participation of Russian affiliated scientists at the > > conference. > > > > The rationale is the as follows: > > > > * The ongoing war in Ukraine is at least partially due to the weak > > response of the Western countries to the Russian invasion of Ukraine > > in 2014 and Georgia in 2008. In fact, the Western countries introduced > > very targeted sanctions which, e.g., banned some Russian officials > > from entering the US (which they did not care about anyway). At the > > same time -- exactly in line with the arguments proposed by the folks > > who want to overturn the decision of ETAPS organisers -- the broad > > Russian population did not bear the burden of the sanctions. Have > > these sanctions helped? No, they have not. In fact, these only > > reassured the Russian regime that the West is "weak" and they can go > > ahead with a fully-fledged war in Ukraine without fearing any > > implications. In other words, all the efforts to change the course of > > actions of the Russian government without negatively impacting the > > Russian population have failed. > > > > * At the same time, upon the commencement of the war in Ukraine, the > > Western governments seem to have learnt the lesson and have devised > > the sanction regime which should hurt the Russian population as a > > whole and make them finally give some thoughts about the decisions of > > their government and the fact that these might be in fact > > counterproductive to their prosperity. This is an unfortunate reality > > that the West has to resolve to this kind of approach, but I believe > > there are only a limited number of ways to stop the war without ending > > up in a direct military confrontation between the West and Russia. > > > > * To everybody who suggests overturning the decision of ETAPS > > organisers I suggest the following thought experiment. Imagine you go > > to bed without knowing you are going to be alive in the morning (as > > Russian army pursues indiscriminate bombing of residential areas; > > including the city of Kharkiv where I grew up). Imagine getting up in > > the morning and calling your relatives to check out whether they are > > still alive. If you were in such a situation, would you still be > > willing to allow the Russian affiliated scientists to participate in > > the conference? This is the reality myself and all the Ukrainians are > > living through. Now, consider whether prohibiting the participation of > > Russian affiliated scientists -- who did not participate at ETAPS en > > masse anyway -- which could bring the end of war a step closer > > outweighs the arguments to let the Russian affiliated scientists > > participate in the conference. > > > > Thanks, Sergiy > > > > > > > > > > > > On Wed, 9 Mar 2022 at 09:50, Alejandro D?az-Caro > > wrote: > > > > > > [ The Types Forum, > http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > > > > > Dear Marino, dear all, > > > > > > El mi?, 9 mar. 2022 05:05, Marino Miculan > > > escribi?: > > > > > > > > > > > Of course, I am sure that there are many colleagues there against the > > > > invasion. But then, we have to distinguish between the > responsibility of > > > > the single, and that of the institution. For instance, I would have > no > > > > problems if a researcher from a Russian university registers and > presents > > > > their results at ETAPS (or any other conference) without any > affiliation. > > > > That would be already a strong signal, as in "I'm here on my own, > and I > > > > dissociate from my rector's opinions". > > > > > > > > > > That would be even worst than the decision of banning a country by > their > > > war politics. What you are proposing there is to ask the researchers > about > > > their political personal opinion in order to be admitted to a > conference. I > > > find this completely wrong. > > > > > > Shall we also inquire Cubans if they support Fidel Castro or Americans > if > > > they support the blockade? Shall we ask Israel or Palestinians what > side of > > > the conflict they support, and let them register according to the > personal > > > stand of the organisers at the venue? > > > > > > I think that mixing politics with the scientific community at this > global > > > level is very dangerous and ultimately wrong. > > > > > > I hope this line of actions do not prosper, or we will damage the > > > scientific community for many years. > > > > > > Best, > > > Alejandro > > > > > > > > From tringer at cs.washington.edu Wed Mar 9 09:30:49 2022 From: tringer at cs.washington.edu (Talia Ringer) Date: Wed, 9 Mar 2022 08:30:49 -0600 Subject: [TYPES] ETAPS bars Russian researchers from attending In-Reply-To: References: Message-ID: 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 cost of isolating academics who happened to be from there. It was sharply controversial at the time among those who were strongly anti-apartheid, and rightly so. Signaling is not worth breaking the ethics code and ruining careers. On Wed, Mar 9, 2022, 5:55 AM Philip Wadler wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > To add to Ricardo's examples, during Apartheid, there was an academic > boycott of South Africa as part of a larger cultural boycott, similar to > the cultural boycott of Russia we see beginning today. This included not > accepting academic visitors affiliated with South Africa, even though many > South African academics opposed Apartheid. Treating Russian institutions > differently at this time can contribute to a cumulative effect. Failing to > treat them differently sends the message that we don't care. Go well, -- P > > > . \ Philip Wadler, Professor of Theoretical Computer Science, > . /\ School of Informatics, University of Edinburgh > . / \ and Senior Research Fellow, IOHK > . > https://urldefense.com/v3/__http://homepages.inf.ed.ac.uk/wadler/__;!!IBzWLUs!ByhpRFSKZ3IGEazSYRk8ZiPNOU_tVRrh8Q_83QpOs_9HzrHFz55B0xkCfLYICuE4ayzyajgRdTs$ > > > > On Tue, 8 Mar 2022 at 20:29, Ricardo Medel > wrote: > > > This email was sent to you by someone outside the University. > > You should only click on links or attachments if you are certain that the > > email is genuine and the content is safe. > > > > [ The Types Forum, > http://lists.seas.upenn.edu/mailman/listinfo/types-list > > ] > > > > German scientists were banned from conferences after the First World War. > > > > Chinese scientists (even those working/studying at the USA) were banned > > from attending a NASA conference in 2013. > > > > > > > > > > El mar., 8 de marzo de 2022 17:25, Gabriel Scherer < > > gabriel.scherer at gmail.com> escribi?: > > > > > [ The Types Forum, > > http://lists.seas.upenn.edu/mailman/listinfo/types-list > > > ] > > > > > > Do people know of any precedent of a conference forbidding people > working > > > in a certain country to attend? > > > > > > (Of course, on a regular basis we hold conferences in countries that > make > > > it difficult for some of our colleagues to attend. But this sounds very > > > different from the conference itself forbidding certain researchers > from > > > attending on the basis of their country of employment.) > > > > > > > > > On Tue, Mar 8, 2022 at 7: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 > > > > > > > > > > The University of Edinburgh is a charitable body, registered in > Scotland, with registration number SC005336. > From fritz at henglein.com Wed Mar 9 11:07:56 2022 From: fritz at henglein.com (Fritz Henglein) Date: Wed, 9 Mar 2022 17:07:56 +0100 Subject: [TYPES] R: ETAPS bars Russian researchers from attending In-Reply-To: References: <9127d0b9-80e5-7c9b-3547-eda22be37ca9@gmail.com> Message-ID: We may very well be in a situation analogous to the Fall of 1939 in Germany: The outbreak of an eventually humongous war, initiated then by an invasion of Poland, now of Ukraine where Ukraine is quite overtly not the final goal, judging by both open announcements and leaked documents out of Moscow; a well-organized dictator with a penchant for effective mass propaganda, enjoying high popularity with a majority determined (or forced to) endure economic isolation and drinking Ersatzkaffee without significant protests; and clever politician speculating (not without reason) that the on-paper-superior Western powers are too indifferent, too afraid or too divided (or any combination of that) to mount an effective resistance. And where researchers and academics are pressured to display allegiance -- or to flee the country. As courageous as the recent joint protest by Russian academics was (as are the ongoing street protests by the few, but stunningly courageous, on the streets of Russia), it *sadly* seems, at this point, that an aloof academic (or sports or cultural) global community will provide more fuel for fostering the impression that the West is harmless and afraid than channeling balanced reporting and openness back and forth across the new bloody iron curtain. My *gut* reaction was that ETAPS overstepped their mandate by being overtly political. On second thought it's hard to see how whatever they -- and others like us organizing events -- decided could *not* be political. Maybe this is the time we should lobby our funding agencies to provide added funding for scientists from Russia and Belarus who may be looking for interesting positions abroad, such as those who may make it to ETAPS somehow (in my mind the sole reason for keeping a sneaky door open to (Bela)Russian participants). At home we and our neighbors are preparing for the arrival of Ukrainian refugees. And of Russian and Belarussian refugees. Fritz On Wed, Mar 9, 2022 at 3:05 PM Sergiy Bogomolov wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > > Banning scientists from ETAPS won't do anything to bring the end of war > a step closer. > > Banning Netflix, McDonalds, Visa, Mastercard, etc., etc., from Russia, > and ceasing to purchase fossil fuels from Russia might. Banning scientific > conferences won't have any impact. > > Alastair: Thanks for your comment. I am afraid I don't really agree > with this statement. > > At this stage, the whole essence of large-scale sanctions is to > inflict pain on the Russian population, with the aim to reduce their > support of the Putin regime. > > In this context, the larger part of the population is targeted, the > more impact sanctions are going to have. > > Russian researchers are part of the whole population and one of the > ways to hit them is to prohibit their participation in international > conferences. > > In other words, I see the step of ETAPS organisers -- similar to > banning Netflix, etc. -- as yet another tool to target a particular > demographic, which the West should deploy to stop the war. > > I hope this makes sense. > > Thanks, Sergiy > > > > > > Cheers > > > > Ally > > > > ________________________________ > > From: Types-list on behalf of > Sergiy Bogomolov > > Sent: 09 March 2022 10:43 > > To: types > > Subject: Re: [TYPES] R: ETAPS bars Russian researchers from attending > > > > [ The Types Forum, > http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > > > Let me start by saying that I strongly support the ETAPS decision to > > ban the participation of Russian affiliated scientists at the > > conference. > > > > The rationale is the as follows: > > > > * The ongoing war in Ukraine is at least partially due to the weak > > response of the Western countries to the Russian invasion of Ukraine > > in 2014 and Georgia in 2008. In fact, the Western countries introduced > > very targeted sanctions which, e.g., banned some Russian officials > > from entering the US (which they did not care about anyway). At the > > same time -- exactly in line with the arguments proposed by the folks > > who want to overturn the decision of ETAPS organisers -- the broad > > Russian population did not bear the burden of the sanctions. Have > > these sanctions helped? No, they have not. In fact, these only > > reassured the Russian regime that the West is "weak" and they can go > > ahead with a fully-fledged war in Ukraine without fearing any > > implications. In other words, all the efforts to change the course of > > actions of the Russian government without negatively impacting the > > Russian population have failed. > > > > * At the same time, upon the commencement of the war in Ukraine, the > > Western governments seem to have learnt the lesson and have devised > > the sanction regime which should hurt the Russian population as a > > whole and make them finally give some thoughts about the decisions of > > their government and the fact that these might be in fact > > counterproductive to their prosperity. This is an unfortunate reality > > that the West has to resolve to this kind of approach, but I believe > > there are only a limited number of ways to stop the war without ending > > up in a direct military confrontation between the West and Russia. > > > > * To everybody who suggests overturning the decision of ETAPS > > organisers I suggest the following thought experiment. Imagine you go > > to bed without knowing you are going to be alive in the morning (as > > Russian army pursues indiscriminate bombing of residential areas; > > including the city of Kharkiv where I grew up). Imagine getting up in > > the morning and calling your relatives to check out whether they are > > still alive. If you were in such a situation, would you still be > > willing to allow the Russian affiliated scientists to participate in > > the conference? This is the reality myself and all the Ukrainians are > > living through. Now, consider whether prohibiting the participation of > > Russian affiliated scientists -- who did not participate at ETAPS en > > masse anyway -- which could bring the end of war a step closer > > outweighs the arguments to let the Russian affiliated scientists > > participate in the conference. > > > > Thanks, Sergiy > > > > > > > > > > > > On Wed, 9 Mar 2022 at 09:50, Alejandro D?az-Caro > > wrote: > > > > > > [ The Types Forum, > http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > > > > > Dear Marino, dear all, > > > > > > El mi?, 9 mar. 2022 05:05, Marino Miculan > > > escribi?: > > > > > > > > > > > Of course, I am sure that there are many colleagues there against the > > > > invasion. But then, we have to distinguish between the > responsibility of > > > > the single, and that of the institution. For instance, I would have > no > > > > problems if a researcher from a Russian university registers and > presents > > > > their results at ETAPS (or any other conference) without any > affiliation. > > > > That would be already a strong signal, as in "I'm here on my own, > and I > > > > dissociate from my rector's opinions". > > > > > > > > > > That would be even worst than the decision of banning a country by > their > > > war politics. What you are proposing there is to ask the researchers > about > > > their political personal opinion in order to be admitted to a > conference. I > > > find this completely wrong. > > > > > > Shall we also inquire Cubans if they support Fidel Castro or Americans > if > > > they support the blockade? Shall we ask Israel or Palestinians what > side of > > > the conflict they support, and let them register according to the > personal > > > stand of the organisers at the venue? > > > > > > I think that mixing politics with the scientific community at this > global > > > level is very dangerous and ultimately wrong. > > > > > > I hope this line of actions do not prosper, or we will damage the > > > scientific community for many years. > > > > > > Best, > > > Alejandro > > > > > > > > From jon at jonmsterling.com Wed Mar 9 11:28:00 2022 From: jon at jonmsterling.com (Jon Sterling) Date: Wed, 9 Mar 2022 17:28:00 +0100 Subject: [TYPES] ETAPS bars Russian researchers from attending In-Reply-To: References: <9127d0b9-80e5-7c9b-3547-eda22be37ca9@gmail.com> Message-ID: <3E7F5356-21BD-4443-B80A-4A8192DDF22A@jonmsterling.com> To other members of the TYPES list, I would like to bring to your attention that I have learned that this has been subject to an editorial style of moderation, so there may be people whose points of view have not been heard because the moderator decided (in his words) that their perspectives "did not add to the discussion". Therefore I would be happy to continue this discussion elsewhere, but I will not be contributing further to this thread. On a broader note, I realize this is a very fraught 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 Henglein wrote: > > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > We may very well be in a situation analogous to the Fall of 1939 in > Germany: The outbreak of an eventually humongous war, initiated then by an > invasion of Poland, now of Ukraine where Ukraine is quite overtly not the > final goal, judging by both open announcements and leaked documents out of > Moscow; a well-organized dictator with a penchant for effective mass > propaganda, enjoying high popularity with a majority determined (or forced > to) endure economic isolation and drinking Ersatzkaffee without significant > protests; and clever politician speculating (not without reason) that the > on-paper-superior Western powers are too indifferent, too afraid or too > divided (or any combination of that) to mount an effective resistance. > > And where researchers and academics are pressured to display allegiance -- > or to flee the country. As courageous as the recent joint protest by > Russian academics was (as are the ongoing street protests by the few, but > stunningly courageous, on the streets of Russia), it *sadly* seems, at this > point, that an aloof academic (or sports or cultural) global community will > provide more fuel for fostering the impression that the West is harmless > and afraid than channeling balanced reporting and openness back and forth > across the new bloody iron curtain. > > My *gut* reaction was that ETAPS overstepped their mandate by being overtly > political. On second thought it's hard to see how whatever they -- and > others like us organizing events -- decided could *not* be political. > Maybe this is the time we should lobby our funding agencies to provide > added funding for scientists from Russia and Belarus who may be looking for > interesting positions abroad, such as those who may make it to ETAPS > somehow (in my mind the sole reason for keeping a sneaky door open to > (Bela)Russian participants). > > At home we and our neighbors are preparing for the arrival of Ukrainian > refugees. And of Russian and Belarussian refugees. > > Fritz > > On Wed, Mar 9, 2022 at 3:05 PM Sergiy Bogomolov wrote: > >> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list >> ] >> >>> Banning scientists from ETAPS won't do anything to bring the end of war >> a step closer. >>> Banning Netflix, McDonalds, Visa, Mastercard, etc., etc., from Russia, >> and ceasing to purchase fossil fuels from Russia might. Banning scientific >> conferences won't have any impact. >> >> Alastair: Thanks for your comment. I am afraid I don't really agree >> with this statement. >> >> At this stage, the whole essence of large-scale sanctions is to >> inflict pain on the Russian population, with the aim to reduce their >> support of the Putin regime. >> >> In this context, the larger part of the population is targeted, the >> more impact sanctions are going to have. >> >> Russian researchers are part of the whole population and one of the >> ways to hit them is to prohibit their participation in international >> conferences. >> >> In other words, I see the step of ETAPS organisers -- similar to >> banning Netflix, etc. -- as yet another tool to target a particular >> demographic, which the West should deploy to stop the war. >> >> I hope this makes sense. >> >> Thanks, Sergiy >> >> >>> >>> Cheers >>> >>> Ally >>> >>> ________________________________ >>> From: Types-list on behalf of >> Sergiy Bogomolov >>> Sent: 09 March 2022 10:43 >>> To: types >>> Subject: Re: [TYPES] R: ETAPS bars Russian researchers from attending >>> >>> [ The Types Forum, >> http://lists.seas.upenn.edu/mailman/listinfo/types-list ] >>> >>> Let me start by saying that I strongly support the ETAPS decision to >>> ban the participation of Russian affiliated scientists at the >>> conference. >>> >>> The rationale is the as follows: >>> >>> * The ongoing war in Ukraine is at least partially due to the weak >>> response of the Western countries to the Russian invasion of Ukraine >>> in 2014 and Georgia in 2008. In fact, the Western countries introduced >>> very targeted sanctions which, e.g., banned some Russian officials >>> from entering the US (which they did not care about anyway). At the >>> same time -- exactly in line with the arguments proposed by the folks >>> who want to overturn the decision of ETAPS organisers -- the broad >>> Russian population did not bear the burden of the sanctions. Have >>> these sanctions helped? No, they have not. In fact, these only >>> reassured the Russian regime that the West is "weak" and they can go >>> ahead with a fully-fledged war in Ukraine without fearing any >>> implications. In other words, all the efforts to change the course of >>> actions of the Russian government without negatively impacting the >>> Russian population have failed. >>> >>> * At the same time, upon the commencement of the war in Ukraine, the >>> Western governments seem to have learnt the lesson and have devised >>> the sanction regime which should hurt the Russian population as a >>> whole and make them finally give some thoughts about the decisions of >>> their government and the fact that these might be in fact >>> counterproductive to their prosperity. This is an unfortunate reality >>> that the West has to resolve to this kind of approach, but I believe >>> there are only a limited number of ways to stop the war without ending >>> up in a direct military confrontation between the West and Russia. >>> >>> * To everybody who suggests overturning the decision of ETAPS >>> organisers I suggest the following thought experiment. Imagine you go >>> to bed without knowing you are going to be alive in the morning (as >>> Russian army pursues indiscriminate bombing of residential areas; >>> including the city of Kharkiv where I grew up). Imagine getting up in >>> the morning and calling your relatives to check out whether they are >>> still alive. If you were in such a situation, would you still be >>> willing to allow the Russian affiliated scientists to participate in >>> the conference? This is the reality myself and all the Ukrainians are >>> living through. Now, consider whether prohibiting the participation of >>> Russian affiliated scientists -- who did not participate at ETAPS en >>> masse anyway -- which could bring the end of war a step closer >>> outweighs the arguments to let the Russian affiliated scientists >>> participate in the conference. >>> >>> Thanks, Sergiy >>> >>> >>> >>> >>> >>> On Wed, 9 Mar 2022 at 09:50, Alejandro D?az-Caro >>> wrote: >>>> >>>> [ The Types Forum, >> http://lists.seas.upenn.edu/mailman/listinfo/types-list ] >>>> >>>> Dear Marino, dear all, >>>> >>>> El mi?, 9 mar. 2022 05:05, Marino Miculan >>>> escribi?: >>>> >>>>> >>>>> Of course, I am sure that there are many colleagues there against the >>>>> invasion. But then, we have to distinguish between the >> responsibility of >>>>> the single, and that of the institution. For instance, I would have >> no >>>>> problems if a researcher from a Russian university registers and >> presents >>>>> their results at ETAPS (or any other conference) without any >> affiliation. >>>>> That would be already a strong signal, as in "I'm here on my own, >> and I >>>>> dissociate from my rector's opinions". >>>>> >>>> >>>> That would be even worst than the decision of banning a country by >> their >>>> war politics. What you are proposing there is to ask the researchers >> about >>>> their political personal opinion in order to be admitted to a >> conference. I >>>> find this completely wrong. >>>> >>>> Shall we also inquire Cubans if they support Fidel Castro or Americans >> if >>>> they support the blockade? Shall we ask Israel or Palestinians what >> side of >>>> the conflict they support, and let them register according to the >> personal >>>> stand of the organisers at the venue? >>>> >>>> I think that mixing politics with the scientific community at this >> global >>>> level is very dangerous and ultimately wrong. >>>> >>>> I hope this line of actions do not prosper, or we will damage the >>>> scientific community for many years. >>>> >>>> Best, >>>> Alejandro >>>> >>>>> >> From bogom.s at gmail.com Wed Mar 9 11:30:40 2022 From: bogom.s at gmail.com (Sergiy Bogomolov) Date: Wed, 9 Mar 2022 16:30:40 +0000 Subject: [TYPES] R: ETAPS bars Russian researchers from attending In-Reply-To: References: <9127d0b9-80e5-7c9b-3547-eda22be37ca9@gmail.com> Message-ID: > In a previous email you said Russian scientists "... did not participate at ETAPS en > masse anyway". Can you explain how excluding them from ETAPS will have any impact on the Russian population (considering also the percentage of the population that belongs to the "computer scientist" category) ? I appreciate that this would be mostly a symbolic step which would illustrate that the whole civilized world stands against Russian aggression. At the same time, will, e.g., Netflix stopping its operations in Russia (as was referenced by Alastair), have any major impact on the outcome of the war? I do not think so. But, if every company and every person does something to oppose Russia, all these actions together will have a huge impact on Russia. In general, if one was to follow the line of reasoning suggested by folks willing to remove the ban on Russian affiliated scientists attending ETAPS, one could pose a question: Shouldn't all international companies just keep their operations Russia and sit out the war? This is about standing on high moral ground and making sure that one does the right thing to stop the war and avoid Ukrainian people being killed -- unfortunately, it seems that there are a number of people in this community who do *not* share these beliefs, which makes me very sad. Thanks, Sergiy > > Best, > Radu > > > On 9 Mar 2022, at 13:43, Sergiy Bogomolov wrote: > > > > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > > >> Banning scientists from ETAPS won't do anything to bring the end of war a step closer. > >> Banning Netflix, McDonalds, Visa, Mastercard, etc., etc., from Russia, and ceasing to purchase fossil fuels from Russia might. Banning scientific conferences won't have any impact. > > > > Alastair: Thanks for your comment. I am afraid I don't really agree > > with this statement. > > > > At this stage, the whole essence of large-scale sanctions is to > > inflict pain on the Russian population, with the aim to reduce their > > support of the Putin regime. > > > > In this context, the larger part of the population is targeted, the > > more impact sanctions are going to have. > > > > Russian researchers are part of the whole population and one of the > > ways to hit them is to prohibit their participation in international > > conferences. > > > > In other words, I see the step of ETAPS organisers -- similar to > > banning Netflix, etc. -- as yet another tool to target a particular > > demographic, which the West should deploy to stop the war. > > > > I hope this makes sense. > > > > Thanks, Sergiy > > > > > >> > >> Cheers > >> > >> Ally > >> > >> ________________________________ > >> From: Types-list on behalf of Sergiy Bogomolov > >> Sent: 09 March 2022 10:43 > >> To: types > >> Subject: Re: [TYPES] R: ETAPS bars Russian researchers from attending > >> > >> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > >> > >> Let me start by saying that I strongly support the ETAPS decision to > >> ban the participation of Russian affiliated scientists at the > >> conference. > >> > >> The rationale is the as follows: > >> > >> * The ongoing war in Ukraine is at least partially due to the weak > >> response of the Western countries to the Russian invasion of Ukraine > >> in 2014 and Georgia in 2008. In fact, the Western countries introduced > >> very targeted sanctions which, e.g., banned some Russian officials > >> from entering the US (which they did not care about anyway). At the > >> same time -- exactly in line with the arguments proposed by the folks > >> who want to overturn the decision of ETAPS organisers -- the broad > >> Russian population did not bear the burden of the sanctions. Have > >> these sanctions helped? No, they have not. In fact, these only > >> reassured the Russian regime that the West is "weak" and they can go > >> ahead with a fully-fledged war in Ukraine without fearing any > >> implications. In other words, all the efforts to change the course of > >> actions of the Russian government without negatively impacting the > >> Russian population have failed. > >> > >> * At the same time, upon the commencement of the war in Ukraine, the > >> Western governments seem to have learnt the lesson and have devised > >> the sanction regime which should hurt the Russian population as a > >> whole and make them finally give some thoughts about the decisions of > >> their government and the fact that these might be in fact > >> counterproductive to their prosperity. This is an unfortunate reality > >> that the West has to resolve to this kind of approach, but I believe > >> there are only a limited number of ways to stop the war without ending > >> up in a direct military confrontation between the West and Russia. > >> > >> * To everybody who suggests overturning the decision of ETAPS > >> organisers I suggest the following thought experiment. Imagine you go > >> to bed without knowing you are going to be alive in the morning (as > >> Russian army pursues indiscriminate bombing of residential areas; > >> including the city of Kharkiv where I grew up). Imagine getting up in > >> the morning and calling your relatives to check out whether they are > >> still alive. If you were in such a situation, would you still be > >> willing to allow the Russian affiliated scientists to participate in > >> the conference? This is the reality myself and all the Ukrainians are > >> living through. Now, consider whether prohibiting the participation of > >> Russian affiliated scientists -- who did not participate at ETAPS en > >> masse anyway -- which could bring the end of war a step closer > >> outweighs the arguments to let the Russian affiliated scientists > >> participate in the conference. > >> > >> Thanks, Sergiy > >> > >> > >> > >> > >> > >> On Wed, 9 Mar 2022 at 09:50, Alejandro D?az-Caro > >> wrote: > >>> > >>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > >>> > >>> Dear Marino, dear all, > >>> > >>> El mi?, 9 mar. 2022 05:05, Marino Miculan > >>> escribi?: > >>> > >>>> > >>>> Of course, I am sure that there are many colleagues there against the > >>>> invasion. But then, we have to distinguish between the responsibility of > >>>> the single, and that of the institution. For instance, I would have no > >>>> problems if a researcher from a Russian university registers and presents > >>>> their results at ETAPS (or any other conference) without any affiliation. > >>>> That would be already a strong signal, as in "I'm here on my own, and I > >>>> dissociate from my rector's opinions". > >>>> > >>> > >>> That would be even worst than the decision of banning a country by their > >>> war politics. What you are proposing there is to ask the researchers about > >>> their political personal opinion in order to be admitted to a conference. I > >>> find this completely wrong. > >>> > >>> Shall we also inquire Cubans if they support Fidel Castro or Americans if > >>> they support the blockade? Shall we ask Israel or Palestinians what side of > >>> the conflict they support, and let them register according to the personal > >>> stand of the organisers at the venue? > >>> > >>> I think that mixing politics with the scientific community at this global > >>> level is very dangerous and ultimately wrong. > >>> > >>> I hope this line of actions do not prosper, or we will damage the > >>> scientific community for many years. > >>> > >>> Best, > >>> Alejandro > >>> > >>>> > From martin.lester at gmail.com Wed Mar 9 11:50:21 2022 From: martin.lester at gmail.com (Martin Lester) Date: Wed, 9 Mar 2022 16:50:21 +0000 Subject: [TYPES] R: ETAPS bars Russian researchers from attending In-Reply-To: References: <9127d0b9-80e5-7c9b-3547-eda22be37ca9@gmail.com> Message-ID: Hi all. Several posters have drawn parallels with other boycotts in the past, academic or otherwise. Sporting boycotts have some similarities. The following philosophy article analyses some arguments for and against sporting boycotts: https://urldefense.com/v3/__https://www.jstor.org/stable/24355089__;!!IBzWLUs!Bj6ROU9fP2NPwtDScWOEWYUhbBp-6u556BwAvDh2T9uOoBFBG-bPKagU7KxMPSU-1Bzs00X4wgk$ Several of the arguments made in the article have also been made in this thread. You may find it insightful. Yours, Martin Lester. From nicolai.kraus at gmail.com Wed Mar 9 13:17:08 2022 From: nicolai.kraus at gmail.com (Nicolai Kraus) Date: Wed, 9 Mar 2022 18:17:08 +0000 Subject: [TYPES] R: ETAPS bars Russian researchers from attending In-Reply-To: References: <9127d0b9-80e5-7c9b-3547-eda22be37ca9@gmail.com> Message-ID: Dear Sergiy, like everyone who has posted on this list, I am absolutely horrified by what is happening in Ukraine, and it is hard for me to even begin to imagine what you are going through. I believe we agree that Putin's regime is to blame, not the Russian population. That's why I feel this statement is not fair: On Wed, Mar 9, 2022 at 12:12 PM Sergiy Bogomolov wrote: > * At the same time, upon the commencement of the war in Ukraine, the > Western governments seem to have learnt the lesson and have devised > the sanction regime which should hurt the Russian population as a > whole and make them finally give some thoughts about the decisions of > their government and the fact that these might be in fact > counterproductive to their prosperity. I don't think researchers in Russia need to be excluded from international events in order to "finally give some thoughts about the decision of their government". I'm worried that such a statement contributes to shifting the blame from the regime to the general population. As far as I'm aware, the huge majority of researchers in Russia oppose Putin's government. Opponents of Putin in- and outside of Russia should work together rather than fight each other. While the Russian government claims to be legitimized through elections, these are not elections according to Western standards. I assume that the support Putin has in the Russian population mostly stems from propaganda and censorship, and researchers attending international conferences are unlikely to be misled. On the contrary, isolating them from the international community might make them more susceptible to censorship. On Wed, Mar 9, 2022 at 12:12 PM Sergiy Bogomolov wrote: > * To everybody who suggests overturning the decision of ETAPS > organisers I suggest the following thought experiment. Imagine you go > to bed without knowing you are going to be alive in the morning (as > Russian army pursues indiscriminate bombing of residential areas; > including the city of Kharkiv where I grew up). Imagine getting up in > the morning and calling your relatives to check out whether they are > still alive. If you were in such a situation, would you still be > willing to allow the Russian affiliated scientists to participate in > the conference? This is the reality myself and all the Ukrainians are > living through. Now, consider whether prohibiting the participation of > Russian affiliated scientists -- who did not participate at ETAPS en > masse anyway -- which could bring the end of war a step closer > outweighs the arguments to let the Russian affiliated scientists > participate in the conference. > This thought is terrifying and I'm deeply sorry that you are in this situation. But if excluding Russian scientists could get us closer to the end of the war, I think many Russian scientists would exclude themselves in a flash. Yes, I would still want to allow Russian-affiliated scientists to attend conferences, please let's not turn this into a "Russians against Ukrainians" situation when it's really "Putin against everyone who is sane". Best wishes, Nicolai (Not sure whether it's relevant, but I'm neither Russian nor Ukrainian.) On Wed, Mar 9, 2022 at 12:12 PM Sergiy Bogomolov wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > Let me start by saying that I strongly support the ETAPS decision to > ban the participation of Russian affiliated scientists at the > conference. > > The rationale is the as follows: > > * The ongoing war in Ukraine is at least partially due to the weak > response of the Western countries to the Russian invasion of Ukraine > in 2014 and Georgia in 2008. In fact, the Western countries introduced > very targeted sanctions which, e.g., banned some Russian officials > from entering the US (which they did not care about anyway). At the > same time -- exactly in line with the arguments proposed by the folks > who want to overturn the decision of ETAPS organisers -- the broad > Russian population did not bear the burden of the sanctions. Have > these sanctions helped? No, they have not. In fact, these only > reassured the Russian regime that the West is "weak" and they can go > ahead with a fully-fledged war in Ukraine without fearing any > implications. In other words, all the efforts to change the course of > actions of the Russian government without negatively impacting the > Russian population have failed. > > * At the same time, upon the commencement of the war in Ukraine, the > Western governments seem to have learnt the lesson and have devised > the sanction regime which should hurt the Russian population as a > whole and make them finally give some thoughts about the decisions of > their government and the fact that these might be in fact > counterproductive to their prosperity. This is an unfortunate reality > that the West has to resolve to this kind of approach, but I believe > there are only a limited number of ways to stop the war without ending > up in a direct military confrontation between the West and Russia. > > * To everybody who suggests overturning the decision of ETAPS > organisers I suggest the following thought experiment. Imagine you go > to bed without knowing you are going to be alive in the morning (as > Russian army pursues indiscriminate bombing of residential areas; > including the city of Kharkiv where I grew up). Imagine getting up in > the morning and calling your relatives to check out whether they are > still alive. If you were in such a situation, would you still be > willing to allow the Russian affiliated scientists to participate in > the conference? This is the reality myself and all the Ukrainians are > living through. Now, consider whether prohibiting the participation of > Russian affiliated scientists -- who did not participate at ETAPS en > masse anyway -- which could bring the end of war a step closer > outweighs the arguments to let the Russian affiliated scientists > participate in the conference. > > Thanks, Sergiy > > > > > > On Wed, 9 Mar 2022 at 09:50, Alejandro D?az-Caro > wrote: > > > > [ The Types Forum, > http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > > > Dear Marino, dear all, > > > > El mi?, 9 mar. 2022 05:05, Marino Miculan > > escribi?: > > > > > > > > Of course, I am sure that there are many colleagues there against the > > > invasion. But then, we have to distinguish between the responsibility > of > > > the single, and that of the institution. For instance, I would have no > > > problems if a researcher from a Russian university registers and > presents > > > their results at ETAPS (or any other conference) without any > affiliation. > > > That would be already a strong signal, as in "I'm here on my own, and I > > > dissociate from my rector's opinions". > > > > > > > That would be even worst than the decision of banning a country by their > > war politics. What you are proposing there is to ask the researchers > about > > their political personal opinion in order to be admitted to a > conference. I > > find this completely wrong. > > > > Shall we also inquire Cubans if they support Fidel Castro or Americans if > > they support the blockade? Shall we ask Israel or Palestinians what side > of > > the conflict they support, and let them register according to the > personal > > stand of the organisers at the venue? > > > > I think that mixing politics with the scientific community at this global > > level is very dangerous and ultimately wrong. > > > > I hope this line of actions do not prosper, or we will damage the > > scientific community for many years. > > > > Best, > > Alejandro > > > > > > From xuanrui at nagoya-u.jp Wed Mar 9 13:43:43 2022 From: xuanrui at nagoya-u.jp (Xuanrui Qi) Date: Thu, 10 Mar 2022 03:43:43 +0900 Subject: [TYPES] R: ETAPS bars Russian researchers from attending In-Reply-To: References: <9127d0b9-80e5-7c9b-3547-eda22be37ca9@gmail.com> Message-ID: <97a450fb30726fc27e44e11d8fd811a3acf12bac.camel@nagoya-u.jp> I think this thread has mostly come to an end, but please let me add my five cents. I agree with Julia on most points. A blanket ban on Russian academics participating in conferences would definitely not help to reduce their minuscule (if an) support for the Putin regime and its aggression. Rather it would probably create more of a sense of isolation and disillusionment. I also find the proposition that reducing the Russian people's support of the Putin regime would bring a halt to its warmongering to be questionable an a bit naive (without offense to anyone). It is simply not true that the Putin regime is in place because there is widespread support in Russia. Most Germans in 1939 definitely weren't Nazis, and most Americans aren't racists either. (I hope I don't get proven wrong on the latter.) But that's to say even in a democracy, one needs to consider a multitude of societal factors before drawing blanket conclusions, and Russia is a country ruled by a dictatorial regime appropriately characterized as fascist. I should also note that many Russian academics have been supporting the anti-war, anti-aggression movement in the face of severe consequences. So, should those academics wish to leave their country and pursue positions in, say, Western Europe, wouldn't ETAPS be an important venue to facilitate these moves? Finally, I would like to add that we should not make this a Russia vs the West issue, or demarcate things along these lines (this sort of thinking offends me quite a bit). Instead this is a matter of conscience. It's warmongering imperialists vs the people, and oppression vs the oppressed. And, at the end of the day, we the people shall prevail, and we will prevail. Best, Xuanrui On Wed, 2022-03-09 at 10:38 -0500, Julia Belyakova wrote: > [ The Types Forum, > http://lists.seas.upenn.edu/mailman/listinfo/types-list?] > > Thank you all for the comments and thoughtful discussion. > > Being a Russian citizen, I don't feel entitled to argue on the ETAPS > decision, and emotionally, I understand the arguments in favor of > that > decision. > I also acknowledge the argument about total isolation of the > population > potentially sending the right message to the population: > > > At this stage, the whole essence of large-scale sanctions is to > > inflict pain on the Russian population, with the aim to reduce > > their > > support of the Putin regime. > > > > In this context, the larger part of the population is targeted, the > > more impact sanctions are going to have. > > > > Russian researchers are part of the whole population and one of the > > ways to hit them is to prohibit their participation in > > international > > conferences. > > However, not all the means help the cause. > > I would like to emphasize that there are a lot of people in Russia > who do > not and have not supported Putin and the ongoing terrible war in > Ukraine. > I think it is not unreasonable to assume that the Russian scientific > community, especially those who used to attend international > conferences > and mingle with the international community, are the ones who are > most > likely to already be in opposition to Putin. > Therefore, I do not see how targeting the population that does not > support > Putin can help with the goal of reducing Putin's support. > Isolation can also make it harder for people to find sources of > information > and see the real picture, playing into Putin's propaganda about the > entire > world hating Russia. Several days ago, the few remaining independent > media > have been blocked or forced to stop writing about the war; Twitter > and > Facebook have been blocked, too, and other platforms are probably > going to > be blocked soon as well. > > Note that Russia is not a democratic country. Normal processes such > as > voting against the regime in an election have not been properly > operating > there for years. Official numbers of overwhelming Putin's support > should be > taken with a sack of salt. > > Since last week, people spreading "misinformation" and "discrediting" > the > Russian army can face up to 15 years in prison. There haven't been > 15-years > convictions yet, but the new law is already working, the first > sentences > have been issued, a number of anti-war protesters have been beaten > and > tortured by the police, the first students have been expelled from > universities for anti-war protests and posts. > Opposing the regime had not been easy even before the new law, and if > you > are interested, I think this thread > < > https://urldefense.com/v3/__https://threadreaderapp.com/thread/1499464 > 037708537861.html__;!!IBzWLUs!FxAKdLfjzQnbTkxz-W3- > 5ggfdA5LYC9B4RvpB_4974izv-urcMH-M6_A5ZAh33U7pVyPl9bIm5U$?> captures > the > situation accurately. > > None of this, of course, compares or lessens the suffering of > Ukrainian > people in any way. > I am devastated and ashamed by Putin's government invasion. > The war is unforgivable. Putin has to be stopped. > > -- > Kind regards, Julia > > > On Wed, Mar 9, 2022 at 9:06 AM Sergiy Bogomolov > wrote: > > > [ The Types Forum, > > http://lists.seas.upenn.edu/mailman/listinfo/types-list > > ] > > > > > Banning scientists from ETAPS won't do anything to bring the end > > > of war > > a step closer. > > > Banning Netflix, McDonalds, Visa, Mastercard, etc., etc., from > > > Russia, > > and ceasing to purchase fossil fuels from Russia might. Banning > > scientific > > conferences won't have any impact. > > > > Alastair: Thanks for your comment. I am afraid I don't really agree > > with this statement. > > > > At this stage, the whole essence of large-scale sanctions is to > > inflict pain on the Russian population, with the aim to reduce > > their > > support of the Putin regime. > > > > In this context, the larger part of the population is targeted, the > > more impact sanctions are going to have. > > > > Russian researchers are part of the whole population and one of the > > ways to hit them is to prohibit their participation in > > international > > conferences. > > > > In other words, I see the step of ETAPS organisers -- similar to > > banning Netflix, etc. -- as yet another tool to target a particular > > demographic, which the West should deploy to stop the war. > > > > I hope this makes sense. > > > > Thanks, Sergiy > > > > > > > > > > Cheers > > > > > > Ally > > > > > > ________________________________ > > > From: Types-list on > > > behalf of > > Sergiy Bogomolov > > > Sent: 09 March 2022 10:43 > > > To: types > > > Subject: Re: [TYPES] R: ETAPS bars Russian researchers from > > > attending > > > > > > [ The Types Forum, > > http://lists.seas.upenn.edu/mailman/listinfo/types-list?] > > > > > > Let me start by saying that I strongly support the ETAPS decision > > > to > > > ban the participation of Russian affiliated scientists at the > > > conference. > > > > > > The rationale is the as follows: > > > > > > *? The ongoing war in Ukraine is at least partially due to the > > > weak > > > response of the Western countries to the Russian invasion of > > > Ukraine > > > in 2014 and Georgia in 2008. In fact, the Western countries > > > introduced > > > very targeted sanctions which, e.g., banned some Russian > > > officials > > > from entering the US (which they did not care about anyway). At > > > the > > > same time -- exactly in line with the arguments proposed by the > > > folks > > > who want to overturn the decision of ETAPS organisers -- the > > > broad > > > Russian population did not bear the burden of the sanctions. Have > > > these sanctions helped? No, they have not. In fact, these only > > > reassured the Russian regime that the West is "weak" and they can > > > go > > > ahead with a fully-fledged war in Ukraine without fearing any > > > implications. In other words, all the efforts to change the > > > course of > > > actions of the Russian government without negatively impacting > > > the > > > Russian population have failed. > > > > > > * At the same time, upon the commencement of the war in Ukraine, > > > the > > > Western governments seem to have learnt the lesson and have > > > devised > > > the sanction regime which should hurt the Russian population as a > > > whole and make them finally give some thoughts about the > > > decisions of > > > their government and the fact? that these might be in fact > > > counterproductive to their prosperity. This is an unfortunate > > > reality > > > that the West has to resolve to this kind of approach, but I > > > believe > > > there are only a limited number of ways to stop the war without > > > ending > > > up in a direct military confrontation between the West and > > > Russia. > > > > > > * To everybody who suggests overturning the decision of ETAPS > > > organisers I suggest the following thought experiment. Imagine > > > you go > > > to bed without knowing you are going to be alive in the morning > > > (as > > > Russian army pursues indiscriminate bombing of residential areas; > > > including the city of Kharkiv where I grew up). Imagine getting > > > up in > > > the morning and calling your relatives to check out whether they > > > are > > > still alive. If you were in such a situation, would you still be > > > willing to allow the Russian affiliated scientists to participate > > > in > > > the conference? This is the reality myself and all the Ukrainians > > > are > > > living through. Now, consider whether prohibiting the > > > participation of > > > Russian affiliated scientists -- who did not participate at ETAPS > > > en > > > masse anyway -- which could bring the end of war a step closer > > > outweighs the arguments to let the Russian affiliated scientists > > > participate in the conference. > > > > > > Thanks, Sergiy > > > > > > > > > > > > > > > > > > On Wed, 9 Mar 2022 at 09:50, Alejandro D?az-Caro > > > wrote: > > > > > > > > [ The Types Forum, > > http://lists.seas.upenn.edu/mailman/listinfo/types-list?] > > > > > > > > Dear Marino, dear all, > > > > > > > > El mi?, 9 mar. 2022 05:05, Marino Miculan > > > > > > > > escribi?: > > > > > > > > > > > > > > Of course, I am sure that there are many colleagues there > > > > > against the > > > > > invasion. But then, we have to distinguish between the > > responsibility of > > > > > the single, and that of the institution.? For instance, I > > > > > would have > > no > > > > > problems if a researcher from a Russian university? registers > > > > > and > > presents > > > > > their results at ETAPS (or any other conference) without any > > affiliation. > > > > > That would be already a strong signal, as in "I'm here on my > > > > > own, > > and I > > > > > dissociate from my rector's opinions". > > > > > > > > > > > > > That would be even worst than the decision of banning a country > > > > by > > their > > > > war politics. What you are proposing there is to ask the > > > > researchers > > about > > > > their political personal opinion in order to be admitted to a > > conference. I > > > > find this completely wrong. > > > > > > > > Shall we also inquire Cubans if they support Fidel Castro or > > > > Americans > > if > > > > they support the blockade? Shall we ask Israel or Palestinians > > > > what > > side of > > > > the conflict they support, and let them register according to > > > > the > > personal > > > > stand of the organisers at the venue? > > > > > > > > I think that mixing politics with the scientific community at > > > > this > > global > > > > level is very dangerous and ultimately wrong. > > > > > > > > I hope this line of actions do not prosper, or we will damage > > > > the > > > > scientific community for many years. > > > > > > > > Best, > > > > Alejandro > > > > > > > > > > > From Alex.Potanin at anu.edu.au Thu Mar 10 13:47:17 2022 From: Alex.Potanin at anu.edu.au (Alex Potanin) Date: Thu, 10 Mar 2022 18:47:17 +0000 Subject: [TYPES] R: ETAPS bars Russian researchers from attending In-Reply-To: References: <9127d0b9-80e5-7c9b-3547-eda22be37ca9@gmail.com> Message-ID: <4E1935A2-B7E6-4F18-A2D7-76D7B172CFF4@anu.edu.au> Hello, One of the only remaining news outlets associated with Russia that is not pro Putin nonsense is Novaya Gazeta (the editor shared the Nobel Peace Prize earlier this year). While I cannot comment on the Russian situation as I have not been there since I left after high school in 1998, I found the following interviews with scientists and IT workers who urgently left for Kyrgizia and Armenia (since you don?t need a Russian Foreign Travel passport to go there) quite insightful. Please use Google Translate: https://urldefense.com/v3/__https://novayagazeta.ru/articles/2022/03/09/ia-bolshe-ne-khochu-pomogat-stroit-eto-gosudarstvo__;!!IBzWLUs!BOlusPmY-hZcXmhj6z3dsUK_tAVGZfAc-8kQqP8HZZqaLN_mtGvezBXdycebT5PlgLy2Ga8GYto$ Ng? mihi nui, Alex. Dr Alex Potanin (he/him) Ahonuku ? Associate Professor Australian National University From tringer at cs.washington.edu Thu Mar 10 16:20:16 2022 From: tringer at cs.washington.edu (Talia Ringer) Date: Thu, 10 Mar 2022 15:20:16 -0600 Subject: [TYPES] R: ETAPS bars Russian researchers from attending In-Reply-To: <4E1935A2-B7E6-4F18-A2D7-76D7B172CFF4@anu.edu.au> References: <9127d0b9-80e5-7c9b-3547-eda22be37ca9@gmail.com> <4E1935A2-B7E6-4F18-A2D7-76D7B172CFF4@anu.edu.au> Message-ID: 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 Ukraine. I hope we as a community will help anyone who wants to get away from Putin's Russia, rather than just punishing the people who are stuck there. On Thu, Mar 10, 2022 at 2:13 PM Alex Potanin wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > Hello, > > One of the only remaining news outlets associated with Russia that is not > pro Putin nonsense is Novaya Gazeta (the editor shared the Nobel Peace > Prize earlier this year). > > While I cannot comment on the Russian situation as I have not been there > since I left after high school in 1998, I found the following interviews > with scientists and IT workers who urgently left for Kyrgizia and Armenia > (since you don?t need a Russian Foreign Travel passport to go there) quite > insightful. Please use Google Translate: > > > https://urldefense.com/v3/__https://novayagazeta.ru/articles/2022/03/09/ia-bolshe-ne-khochu-pomogat-stroit-eto-gosudarstvo__;!!IBzWLUs!BOlusPmY-hZcXmhj6z3dsUK_tAVGZfAc-8kQqP8HZZqaLN_mtGvezBXdycebT5PlgLy2Ga8GYto$ > > Ng? mihi nui, > Alex. > > Dr Alex Potanin (he/him) > Ahonuku ? Associate Professor > Australian National University > > From ijdt.editor at gmail.com Thu Mar 10 15:20:27 2022 From: ijdt.editor at gmail.com (Apostolos Syropoulos) Date: Thu, 10 Mar 2022 22:20:27 +0200 Subject: [TYPES] R: ETAPS bars Russian researchers from attending In-Reply-To: <97a450fb30726fc27e44e11d8fd811a3acf12bac.camel@nagoya-u.jp> References: <9127d0b9-80e5-7c9b-3547-eda22be37ca9@gmail.com> <97a450fb30726fc27e44e11d8fd811a3acf12bac.camel@nagoya-u.jp> Message-ID: Hi people, I would like to make a comment that is closely related to this ongoing discussion. Turkey is another country that has invaded a third country, namely Cyprus, but I haven't noticed a similar sensitivity against Turkey. Just for your information, Turkey invaded and still occupies 35% of the island in 1974. Their excuse was the one used by Russia: To protect people that they considered their own people. In addition, we should not forget that Erdogan is Turkey's Putin: He jails people with no excuse, he has invaded to Syria, he oppresses Kurds [speaking the Kurdish language is prohibited and giving the name Yolda? (comrade in Turkish but a common Kurdish name) to a kid is like a crime...], he censors everyone and yet most "scientists" find all these quite reasonable! This is the apotheosis of hypocrisy! Regards, Apostolos Syropoulos -- Apostolos Syropoulos Xanthi, GREECE Web-page at https://urldefense.com/v3/__http://asyropoulos.eu__;!!IBzWLUs!DG-S4rbDUXjibVz8Wzwqk3vww2LGc92SdWQSfAJj6hXrMxkxskP3_y4bRYKqLmMuAa1KrMxLUOU$ Blogs at https://urldefense.com/v3/__http://asyropoulos.wordpress.com/__;!!IBzWLUs!DG-S4rbDUXjibVz8Wzwqk3vww2LGc92SdWQSfAJj6hXrMxkxskP3_y4bRYKqLmMuAa1K13gLv9w$ https://urldefense.com/v3/__http://hypercomputation.blogspot.com/__;!!IBzWLUs!DG-S4rbDUXjibVz8Wzwqk3vww2LGc92SdWQSfAJj6hXrMxkxskP3_y4bRYKqLmMuAa1KLYAEdwc$ From xuanrui at nagoya-u.jp Fri Mar 11 01:56:34 2022 From: xuanrui at nagoya-u.jp (Xuanrui Qi) Date: Fri, 11 Mar 2022 15:56:34 +0900 Subject: [TYPES] R: ETAPS bars Russian researchers from attending In-Reply-To: References: <9127d0b9-80e5-7c9b-3547-eda22be37ca9@gmail.com> <97a450fb30726fc27e44e11d8fd811a3acf12bac.camel@nagoya-u.jp> Message-ID: <7194aafd033ff1ceeb2b78064bf1cd7fa34aa9c4.camel@nagoya-u.jp> Or Israel. Not only that no one has ever called on prohibiting Israeli scientists from participating in conferences (fortunately), but conferences have also been held in Israel, which is a poor call and unacceptable to me. (For instance, would participants of Arab descent feel safe and welcome? I don't think so... Personally I don't really want to go there either.) It is wrong to ban people from participating in a *scientific* conference based on their nationality, affiliation or political views. It's especially wrong to prevent their attendance because they *fail to express support for a certain view*, as some people have dangerously suggested in this thread. But we should nevertheless adopt an equal standard of scrutiny in all cases, and when that's not possible, at least make the rationale (to why equal standards could not be maintained) known. -Xuanrui On Thu, 2022-03-10 at 22:20 +0200, Apostolos Syropoulos wrote: > [ The Types Forum, > http://lists.seas.upenn.edu/mailman/listinfo/types-list?] > > Hi people, > > I would like to make a comment that is closely related to this > ongoing > discussion. > Turkey is another country that has invaded a third country, namely > Cyprus, > but I > haven't noticed a similar sensitivity against Turkey. Just for your > information, Turkey > invaded and still occupies 35% of the island in 1974. Their excuse > was the > one used > by Russia: To protect people that they considered their own people. > In > addition, > we should not forget that Erdogan is Turkey's Putin: He jails people > with > no excuse, he > has invaded to Syria, he oppresses Kurds [speaking the Kurdish > language is > prohibited > and giving the name Yolda? (comrade in Turkish but a common Kurdish > name) > to a kid > is like a crime...], he censors everyone and yet most "scientists" > find all > these quite > ?reasonable! This is the apotheosis of hypocrisy! > > Regards, > > Apostolos Syropoulos > From ross.horne at gmail.com Fri Mar 11 04:28:37 2022 From: ross.horne at gmail.com (Ross Horne) Date: Fri, 11 Mar 2022 10:28:37 +0100 Subject: [TYPES] R: ETAPS bars Russian researchers from attending In-Reply-To: <7194aafd033ff1ceeb2b78064bf1cd7fa34aa9c4.camel@nagoya-u.jp> References: <9127d0b9-80e5-7c9b-3547-eda22be37ca9@gmail.com> <97a450fb30726fc27e44e11d8fd811a3acf12bac.camel@nagoya-u.jp> <7194aafd033ff1ceeb2b78064bf1cd7fa34aa9c4.camel@nagoya-u.jp> Message-ID: There are too many different views on parallel conflicts, so I'm sticking to Russia-Ukraine and conferences such as ETAPS. Although the policy has been updated, there are still things to do: 1. On Russians academics: Russian academics are also scared. At least 99% of them are in the well-informed category, are therefore appalled by the war, and suffering restrictions, e.g., they are eligible for conscription in a conflict they do not support, and may be cut off from relatives. I support high level sanctions of people in the public eye, but CS researchers (unlike rectors) are not in the public eye, so sanctioning researchers would serve no good. We should be supporting these researchers. If there is a submitted paper "of political concern", from Russia (or any other country), we can have confidence that it will be filtered out by the review process without needing to update the code of conduct for conferences. 2. On Ukrainian academics: universities will have ceased functioning and have even been bombed. What ETAPS can consider is forming a committee to discuss how we can *support* the intellectual reconstruction of Ukraine going forwards. Today, we cannot possibly know the best way to proceed. However, round tables can be arranged and committees can be formed to address this question. For example, if genuine stability returns even to part of Ukraine, we, as a community, can help as visiting researchers to rebuild departments. We can also include universities in funding applications. To achieve this, stakeholders such as funding agencies and Ukrainian scientists, would need to be engaged soon for strategic readiness, rather than waiting until the solution is clearer. Why funding agencies? If they are not engaged they will not be prepared to assist, and are likely to consider adding a partner institution in Ukraine to a project as an untenable risk, rather than a major humanitarian contribution and hence points for funding a project (although not as the sole criterion of course). It seems that a conference should host this debate. Since ETAPS have gone political, perhaps they are best positioned for initiating such a proactive debate. Kind regards, Ross From gabriel.scherer at gmail.com Fri Mar 11 08:27:37 2022 From: gabriel.scherer at gmail.com (Gabriel Scherer) Date: Fri, 11 Mar 2022 14:27:37 +0100 Subject: [TYPES] ETAPS bars Russian researchers from attending In-Reply-To: References: Message-ID: Dear list, types-list moderator here: I have received a request to close this thread for further discussion, for the reason that continued discussions can cause pain to some of our colleagues. I have not made any decision yet, but I understand the broad argument of benefits/costs ratio: the original decision by ETAPS has been reversed, and we may be seeing diminishing returns in continued discussions -- yet I admire the last post by Ross Horne, http://lists.seas.upenn.edu/pipermail/types-list/2022/002432.html , which may also be an opening for related but different discussions, possibly in different venues. I will consult with past moderators. In any case, please carefully consider whether any further post is really necessary for the discussion. As noted previously by Jon Sterling ( http://lists.seas.upenn.edu/pipermail/types-list/2022/002423.html ), this discussion has been the occasion for some of you to realize that the moderation of types-list is in part an editorial process: it's not just filtering obvious spam, sometimes messages are not forwarded for other reasons (including: not adding enough to the discussion, or risking a spiralling towards bad-quality discussions). I've received feedback that people are not aware of this (and that this moderation style is not to everyone's liking) -- thanks! I will edit the list description page to make this clear, and discuss moderation approaches with past moderators. There is a thread on the Types Zulip ( typ.zulipchat.com/ ) discussing types-list moderation. Feel free to participate there, but I wish to avoid long meta-discussions on the mailing-list itself. Many mailing-list users react negatively to voluminous discussions, especially on topics that they consider less appropriate or less useful. In general, Zulip makes it easier for average users to tune out of conversations, and has an explicit "miscellaneous" category that includes meta- discussions. (There is no a-priori moderation of messages on Zulip.) Finally, I wish to thank everyone for this discussion. This is a very difficult topic, and it could have gone very badly. I'm sure we could have done better, and we will need more time to discuss and reflect. Yet we were able to collectively express ourselves, on a controversial topic, during a very difficult time; an accomplishment. Best, and with thoughts to the many people affected, directly or indirectly, by this war. On Tue, Mar 8, 2022 at 7: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 > From vamchale at gmail.com Sat Mar 19 19:40:35 2022 From: vamchale at gmail.com (Vanessa McHale) Date: Sat, 19 Mar 2022 18:40:35 -0500 Subject: [TYPES] =?utf-8?q?Annotating_an_AST_with_=28existential=29_types?= =?utf-8?q?=2C_with_ordered_contexts_-_=C3=A0_la_Dunfield_Krishnaswami?= Message-ID: <0FD412DE-FCE0-482C-9860-02B9ECB472CC@gmail.com> Hi all, I am trying to write a compiler with existential types. I understand that the Dunfield-Krishnaswami approach with ordered contexts is the new/cool way to do type inference. However, I am stumped as to how to annotate a term with all the solved variables (when using ordered contexts). Is this possible? Is there any guidance/existing literature? As an example, I?d like to be able to know/use the type of f in the below: (?f. (f (?x. x)) (f ())) (?x. x) Thanks, Vanessa McHale From aaronngray.lists at gmail.com Sat Mar 19 23:47:04 2022 From: aaronngray.lists at gmail.com (Aaron Gray) Date: Sun, 20 Mar 2022 03:47:04 +0000 Subject: [TYPES] Mendler's paper - Recursive Types and Type Constraints in Second-Order Lambda Calculus Message-ID: Trying to find a copy of :- MENDLER, N. P. 1987. Recursive Types and Type Constraints in Second-Order Lambda Calculus -- Aaron Gray From rdbrown0au at gmail.com Sat Apr 23 03:57:33 2022 From: rdbrown0au at gmail.com (Rodney Brown) Date: Sat, 23 Apr 2022 17:57:33 +1000 Subject: [TYPES] "Type systems for programs respecting dimensions" Re: Types for Units-of-Measure In-Reply-To: References: Message-ID: <0e507ad0-bc2e-effa-be57-b80fc3336dd3@gmail.com> For people who are interested :- McBride, Conor; Nordvall-Forsberg, Fredrik (2022). "Type systems for programs respecting dimensions" (PDF). Advanced Mathematical and Computational Tools in Metrology and Testing XII. Advances in Mathematics for Applied Sciences. World Scientific. pp. 331?345. doi:10.1142/9789811242380_0020. ISBN 9789811242380. https://urldefense.com/v3/__https://pureportal.strath.ac.uk/files/121022760/McBride_etal_amctmtxii2021_type_systems_for_programs_respecting_dimensions.pdf__;!!IBzWLUs!UX9RGwE5FC7pDxN47lDwNSXSAGRQyL5BgEzF1Jh82ctFk29TRks-axesIRwfnSzjWQsnkE7KCbhahp8xI9WTIixy-7kG5YI$ From the Conclusion: Following Hart, we have shown how to use dependent types to extend type systems for units of measure from scalars to matrices. ... On 9/11/20 22:42, Rodney Brown wrote: > Reading ACM SigPlan Notices in the 80s, the papers on adding > Units-of-Measure to programming > languages for type-checking seemed sensible - especially after reading > Comp.risks in > Software Engineering Notes. > > More recently I read George Hart's 1995 book "Multidimensional > Analysis: ..." which provided > the abstract algebra behind my vague intuitive understanding of > Dimensional correctness, > sketched an implementation and described the suprising (to me) result > that some problems in > science and engineering need matrices that aren't simply dimensionally > uniform. From gabriel.scherer at gmail.com Thu May 12 04:42:05 2022 From: gabriel.scherer at gmail.com (Gabriel Scherer) Date: Thu, 12 May 2022 10:42:05 +0200 Subject: [TYPES] [meta] URL rewriting notice In-Reply-To: References: Message-ID: Dear types-list, (list moderator here; I'm replying to a [meta] message I sent to types-announce in July 2021, which you may want to read below for context.) I have received several emails from list members over the last month(s) about getting types-{list,announce} marked as spam on your end, or receiving worrying automated emails from the list about your membership being disabled "due to excessive bounces". Thanks for your reports! Unfortunately, I believe that there is nothing I have changed or can change on my end to fix this. My best guess is that it comes from UPenn mailing-list sysadmin changes, possibly the change of August 2021 to add URL filtering/rewriting (that I suspect interacts badly with security / anti-spam measures, but didn't have this current effect at the time), possibly some later change that I don't know about. I wrote to the UPenn people to ask for help; but in August 2021 they were not able to provide any help, and I am not confident that it will be different this time. We may have to migrate to a different mailing-list host in the coming months. (Only a dozen of people gave their opinion in August 2021, but those that did were generally in support of changing mailing-list provider to avoid the unpleasant practice of URL filtering. I have not acted on these suggestions, partly out of personal laziness, but also because I worry that the transition would be fairly disruptive for list members.) My own employer (INRIA, in France) has a mailing-list service that could probably be used. If you have recommendations -- if your university insists on doing the world a favor by hosting academic mailing lists -- now may be a good time to send them to me. I will also consult with past moderators for guidance. Listly yours, cheers On Fri, Aug 13, 2021 at 3:55 PM Gabriel Scherer wrote: > Dear types-announce list, > > UPenn, who has been generously hosting this mailing-list (and types-list) > since 2006, has just setup an email-processing system that rewrites URLs > included in all email received by the university, including their > mailing-list services, "protecting" them by turning them into a reference > to a third-party service (ProofPoint / urldefense) that should redirect to > the intended URL after some unknown security-inspired procedures have been > applied -- or block access because someone's filter is wrong. > > We are in touch with the administrators to try to disable this > transformation, but in the meantime I decided to keep forwarding the emails > as usual to avoid disrupting the flow of announcements. Apologies in > advance for the strange, modified URLs, and the inconvenience it may cause > (mailing-list email being marked as spam due to failed DKIM verification, > etc.). > > Best > From jung at mpi-sws.org Thu May 12 05:57:28 2022 From: jung at mpi-sws.org (Ralf Jung) Date: Thu, 12 May 2022 11:57:28 +0200 Subject: [TYPES] [meta] URL rewriting notice In-Reply-To: References: Message-ID: <908802ff-7c65-97cf-75cb-1112a245f2f1@mpi-sws.org> Hi all, > We may have to migrate to a different mailing-list host in the coming > months. (Only a dozen of people gave their opinion in August 2021, but > those that did were generally in support of changing mailing-list provider > to avoid the unpleasant practice of URL filtering. I have not acted on > these suggestions, partly out of personal laziness, but also because I > worry that the transition would be fairly disruptive for list members.) > My own employer (INRIA, in France) has a mailing-list service that could > probably be used. If you have recommendations -- if your university insists > on doing the world a favor by hosting academic mailing lists -- now may be > a good time to send them to me. I will also consult with past moderators > for guidance. This may be a bit far out there, but another potential alternative to consider is to use Discourse. Discourse is a forum software with a mailing list mode, combining the best of web-based forums and mail-based lists. In mailing list mode it behaves basically like a mailing list, but if you use it as a forum then you only subscribe to topics you are interested in (plus hourly/daily/weekly summaries of new topics; you can also subscribe to everything in a "category"). Being a forum it also has much better search than any mailing list I have seen, and one can very easily reply to topics that were created before one joined, or read a thread of discussion later. For higher-traffic lists, I think Discourse is clearly better (and e.g. LLVM recently switched their development mailing list to discourse; Rust is also using Discourse rather than a mailing list). TYPES is very low-traffic though, so the point is much less clear. OTOH I think this might help mitigate some of the concerns people have with occasional spikes of discussion like we had recently, where IIRC one concern was that people generally expect this to be low-traffic. Kind regards, Ralf > > Listly yours, cheers > > On Fri, Aug 13, 2021 at 3:55 PM Gabriel Scherer > wrote: > >> Dear types-announce list, >> >> UPenn, who has been generously hosting this mailing-list (and types-list) >> since 2006, has just setup an email-processing system that rewrites URLs >> included in all email received by the university, including their >> mailing-list services, "protecting" them by turning them into a reference >> to a third-party service (ProofPoint / urldefense) that should redirect to >> the intended URL after some unknown security-inspired procedures have been >> applied -- or block access because someone's filter is wrong. >> >> We are in touch with the administrators to try to disable this >> transformation, but in the meantime I decided to keep forwarding the emails >> as usual to avoid disrupting the flow of announcements. Apologies in >> advance for the strange, modified URLs, and the inconvenience it may cause >> (mailing-list email being marked as spam due to failed DKIM verification, >> etc.). >> >> Best >> -- Website: https://urldefense.com/v3/__https://ralfj.de/research__;!!IBzWLUs!RXKu6AzQyKnk0mm4ucqeheRdTrOm1nMYErzL9mXosBkKZWy38pcogdrZtMBWV4Fi4RC2iSRJCekxCpdFaOytpWpl5Q$ From lists at richarde.dev Thu May 12 09:36:15 2022 From: lists at richarde.dev (Richard Eisenberg) Date: Thu, 12 May 2022 13:36:15 +0000 Subject: [TYPES] [meta] URL rewriting notice In-Reply-To: <908802ff-7c65-97cf-75cb-1112a245f2f1@mpi-sws.org> References: <908802ff-7c65-97cf-75cb-1112a245f2f1@mpi-sws.org> Message-ID: <010f0180b87bfe35-509f8fc0-3b89-468d-9c36-53351f5c9d49-000000@us-east-2.amazonses.com> As a happy user of mailing lists and a skeptic of tools like Discourse, I've been reasonably pleased with my recent use of Discourse for some Haskell-related communication. The mailing list mode works well, and I imagine most of us can settle into using Discourse much like we use the current mailing list. Discourse has some settings that may need careful attention (e.g. it likes to limit posts to contain only 2 links until the poster has gained some level of reputation in the system), but I imagine these can be tuned to our liking. Richard > On May 12, 2022, at 5:57 AM, Ralf Jung wrote: > > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Hi all, > >> We may have to migrate to a different mailing-list host in the coming >> months. (Only a dozen of people gave their opinion in August 2021, but >> those that did were generally in support of changing mailing-list provider >> to avoid the unpleasant practice of URL filtering. I have not acted on >> these suggestions, partly out of personal laziness, but also because I >> worry that the transition would be fairly disruptive for list members.) >> My own employer (INRIA, in France) has a mailing-list service that could >> probably be used. If you have recommendations -- if your university insists >> on doing the world a favor by hosting academic mailing lists -- now may be >> a good time to send them to me. I will also consult with past moderators >> for guidance. > > This may be a bit far out there, but another potential alternative to consider is to use Discourse. Discourse is a forum software with a mailing list mode, combining the best of web-based forums and mail-based lists. In mailing list mode it behaves basically like a mailing list, but if you use it as a forum then you only subscribe to topics you are interested in (plus hourly/daily/weekly summaries of new topics; you can also subscribe to everything in a "category"). Being a forum it also has much better search than any mailing list I have seen, and one can very easily reply to topics that were created before one joined, or read a thread of discussion later. > > For higher-traffic lists, I think Discourse is clearly better (and e.g. LLVM recently switched their development mailing list to discourse; Rust is also using Discourse rather than a mailing list). > TYPES is very low-traffic though, so the point is much less clear. OTOH I think this might help mitigate some of the concerns people have with occasional spikes of discussion like we had recently, where IIRC one concern was that people generally expect this to be low-traffic. > > Kind regards, > Ralf > >> Listly yours, cheers >> On Fri, Aug 13, 2021 at 3:55 PM Gabriel Scherer >> wrote: >>> Dear types-announce list, >>> >>> UPenn, who has been generously hosting this mailing-list (and types-list) >>> since 2006, has just setup an email-processing system that rewrites URLs >>> included in all email received by the university, including their >>> mailing-list services, "protecting" them by turning them into a reference >>> to a third-party service (ProofPoint / urldefense) that should redirect to >>> the intended URL after some unknown security-inspired procedures have been >>> applied -- or block access because someone's filter is wrong. >>> >>> We are in touch with the administrators to try to disable this >>> transformation, but in the meantime I decided to keep forwarding the emails >>> as usual to avoid disrupting the flow of announcements. Apologies in >>> advance for the strange, modified URLs, and the inconvenience it may cause >>> (mailing-list email being marked as spam due to failed DKIM verification, >>> etc.). >>> >>> Best >>> > > -- > Website: https://urldefense.com/v3/__https://ralfj.de/research__;!!IBzWLUs!RXKu6AzQyKnk0mm4ucqeheRdTrOm1nMYErzL9mXosBkKZWy38pcogdrZtMBWV4Fi4RC2iSRJCekxCpdFaOytpWpl5Q$ From gabriel.scherer at gmail.com Sat May 14 09:48:35 2022 From: gabriel.scherer at gmail.com (Gabriel Scherer) Date: Sat, 14 May 2022 15:48:35 +0200 Subject: [TYPES] [meta] URL rewriting notice In-Reply-To: <010f0180b87bfe35-509f8fc0-3b89-468d-9c36-53351f5c9d49-000000@us-east-2.amazonses.com> References: <908802ff-7c65-97cf-75cb-1112a245f2f1@mpi-sws.org> <010f0180b87bfe35-509f8fc0-3b89-468d-9c36-53351f5c9d49-000000@us-east-2.amazonses.com> Message-ID: Thanks everyone for the feedback, The UPenn admins have fixed something in the way they implement URL rewriting, and I hope that the "marked as SPAM or bounced" inconveniences that several of you have have experienced should go away. Please let me know (off-list) if you are affected again. (Also: thanks to Benjamin Pierce for his help talking with the UPenn people.) Thanks for the feedback on Discourse. Currently we have a mailing-list that is the same as existed twenty years ago, and as an alternative the Zulip that is modern, shiny, has an application for smartphones, etc. Some people prefer the mailing-list (in jest one would say "senior members of our community"), some the Zulip. I would be hesitant of just adding a third place, and I don't know whether Discourse should be considered as a replacement for the mailing-list, or Zulip, or both. Discourse is a nice tool, but I don't know that it would work as well as the mailing-list in the role of "reliable old tool". For example: we have mailing-list archives from 2003 onward in a single place (and older archives one URL away), how many web forums have 20 years of archives? Conversely, I can see several ways in which it improves over Zulip (better searchability, mature moderation tools), but it loses in terms of immediateness / "instant chat" feeling -- it looks like the Coq Discourse is seeing much lower volume than the Coq Zulip, perhaps for these subtle fuzzy reasons. (On the other hand, the experience of the OCaml community migrating from a mailing-list to Discourse was fairly positive.) Long story short: nothing that is not a mailing-list is a clear improvement over a mailing-list for scholarly discussions, so my intuition is to be conservative and keep the mailing-list working while we can. We can reconsider in the future if there is clear demand, or if there are signs that the mailing-list is dying, or if it starts malfunctioning again. Cheers On Thu, May 12, 2022 at 4:08 PM Richard Eisenberg wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > As a happy user of mailing lists and a skeptic of tools like Discourse, > I've been reasonably pleased with my recent use of Discourse for some > Haskell-related communication. The mailing list mode works well, and I > imagine most of us can settle into using Discourse much like we use the > current mailing list. Discourse has some settings that may need careful > attention (e.g. it likes to limit posts to contain only 2 links until the > poster has gained some level of reputation in the system), but I imagine > these can be tuned to our liking. > > Richard > > > On May 12, 2022, at 5:57 AM, Ralf Jung wrote: > > > > [ The Types Forum, > http://lists.seas.upenn.edu/mailman/listinfo/types-list < > http://lists.seas.upenn.edu/mailman/listinfo/types-list> ] > > > > Hi all, > > > >> We may have to migrate to a different mailing-list host in the coming > >> months. (Only a dozen of people gave their opinion in August 2021, but > >> those that did were generally in support of changing mailing-list > provider > >> to avoid the unpleasant practice of URL filtering. I have not acted on > >> these suggestions, partly out of personal laziness, but also because I > >> worry that the transition would be fairly disruptive for list members.) > >> My own employer (INRIA, in France) has a mailing-list service that could > >> probably be used. If you have recommendations -- if your university > insists > >> on doing the world a favor by hosting academic mailing lists -- now may > be > >> a good time to send them to me. I will also consult with past moderators > >> for guidance. > > > > This may be a bit far out there, but another potential alternative to > consider is to use Discourse. Discourse is a forum software with a mailing > list mode, combining the best of web-based forums and mail-based lists. In > mailing list mode it behaves basically like a mailing list, but if you use > it as a forum then you only subscribe to topics you are interested in (plus > hourly/daily/weekly summaries of new topics; you can also subscribe to > everything in a "category"). Being a forum it also has much better search > than any mailing list I have seen, and one can very easily reply to topics > that were created before one joined, or read a thread of discussion later. > > > > For higher-traffic lists, I think Discourse is clearly better (and e.g. > LLVM recently switched their development mailing list to discourse; Rust is > also using Discourse rather than a mailing list). > > TYPES is very low-traffic though, so the point is much less clear. OTOH > I think this might help mitigate some of the concerns people have with > occasional spikes of discussion like we had recently, where IIRC one > concern was that people generally expect this to be low-traffic. > > > > Kind regards, > > Ralf > > > >> Listly yours, cheers > >> On Fri, Aug 13, 2021 at 3:55 PM Gabriel Scherer < > gabriel.scherer at gmail.com> > >> wrote: > >>> Dear types-announce list, > >>> > >>> UPenn, who has been generously hosting this mailing-list (and > types-list) > >>> since 2006, has just setup an email-processing system that rewrites > URLs > >>> included in all email received by the university, including their > >>> mailing-list services, "protecting" them by turning them into a > reference > >>> to a third-party service (ProofPoint / urldefense) that should > redirect to > >>> the intended URL after some unknown security-inspired procedures have > been > >>> applied -- or block access because someone's filter is wrong. > >>> > >>> We are in touch with the administrators to try to disable this > >>> transformation, but in the meantime I decided to keep forwarding the > emails > >>> as usual to avoid disrupting the flow of announcements. Apologies in > >>> advance for the strange, modified URLs, and the inconvenience it may > cause > >>> (mailing-list email being marked as spam due to failed DKIM > verification, > >>> etc.). > >>> > >>> Best > >>> > > > > -- > > Website: > https://urldefense.com/v3/__https://ralfj.de/research__;!!IBzWLUs!RXKu6AzQyKnk0mm4ucqeheRdTrOm1nMYErzL9mXosBkKZWy38pcogdrZtMBWV4Fi4RC2iSRJCekxCpdFaOytpWpl5Q$ > < > https://urldefense.com/v3/__https://ralfj.de/research__;!!IBzWLUs!RXKu6AzQyKnk0mm4ucqeheRdTrOm1nMYErzL9mXosBkKZWy38pcogdrZtMBWV4Fi4RC2iSRJCekxCpdFaOytpWpl5Q$ > > > From monnier at iro.umontreal.ca Fri May 20 21:16:42 2022 From: monnier at iro.umontreal.ca (Stefan Monnier) Date: Fri, 20 May 2022 21:16:42 -0400 Subject: [TYPES] Writing syntactic models with "full information" Message-ID: I often write translations between PTS-style languages where the overall structure of the translation can be represented by saying that an input expression `e` is turned into an output `[e]` with a property like ? ? e : ? => [?] ? [e] : [?] Or some variant of it, very much like Boulier et al. did in "The next 700 syntactical models of type theory". But often my translation function [?] needs a bit more info than that provided by an expression. E.g. it may need to know the expression's type or the typing context in which it was found. So what I end up doing is to define my translation function as taking a typing derivation as input while still returning a mere expression. Formally it means the above elegant property becomes: ? ? e : ? (which implies that ??. ? ? ? : Type?) => [?] ? [? ? e : ?] : [? ? ? : Type?] which is much less elegant and less friendly for the reader (I did something like that for example in "Inductive types deconstructed: the calculus of united constructions" and this was mentioned as an oddity by one of the reviewers, for example). It also makes the presentation more verbose and harder to read, for which the only way out I have found is to use cringe-worthy abuses of notation where I might write [e] as a shorthand for [? ? e : ?] where the ? and ? are presumed "obvious from context". Has anyone here faced similar issues? What's a better approach? Stefan From c.mclaughlin at unsw.edu.au Sun May 22 20:02:39 2022 From: c.mclaughlin at unsw.edu.au (Craig McLaughlin) Date: Mon, 23 May 2022 10:02:39 +1000 Subject: [TYPES] Writing syntactic models with "full information" In-Reply-To: References: Message-ID: <96a7b2c7-2a77-8ab9-119a-4a8f98cb1893@unsw.edu.au> Hi Stefan, I see quite a number of logical relations-based models define functions of the form [| ? ? e : ? |] which then use the context and type of e as needed. Such a function could be seen to be defined on well-typed and well-scoped expressions[1] where (the usually implicit) ? and ? are made explicit. Of course, if you are dealing with extrinsic (as opposed to intrinsic above) syntax this viewpoint may be of little help. [1] - Allais et al. ?A Type and Scope Safe Universe of Syntaxes with Binding, Their Semantics and Proofs? 9, no. 4 (n.d.): 30. On 21/5/22 11:16, Stefan Monnier wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > I often write translations between PTS-style languages where the overall > structure of the translation can be represented by saying that an input > expression `e` is turned into an output `[e]` with a property like > > ? ? e : ? > => > [?] ? [e] : [?] > > Or some variant of it, very much like Boulier et al. did in "The next > 700 syntactical models of type theory". > > But often my translation function [?] needs a bit more info than that > provided by an expression. E.g. it may need to know the expression's > type or the typing context in which it was found. So what I end up > doing is to define my translation function as taking a typing derivation > as input while still returning a mere expression. > > Formally it means the above elegant property becomes: > > ? ? e : ? (which implies that ??. ? ? ? : Type?) > => > [?] ? [? ? e : ?] : [? ? ? : Type?] > > which is much less elegant and less friendly for the reader (I did > something like that for example in "Inductive types deconstructed: the > calculus of united constructions" and this was mentioned as an oddity > by one of the reviewers, for example). > > It also makes the presentation more verbose and harder to read, for > which the only way out I have found is to use cringe-worthy abuses of > notation where I might write [e] as a shorthand for [? ? e : ?] where > the ? and ? are presumed "obvious from context". > > Has anyone here faced similar issues? What's a better approach? > > > Stefan > From jonathanhwchan at gmail.com Mon May 23 00:40:54 2022 From: jonathanhwchan at gmail.com (Jonathan Chan) Date: Sun, 22 May 2022 21:40:54 -0700 Subject: [TYPES] Writing syntactic models with "full information" In-Reply-To: References: Message-ID: In Compiling with Dependent Types the translations that depend on the typing derivation (looking at 6.5 or 5.3 for instance) are defined as judgements, e.g. ? ? A : ?' ? *A* ?, x: A ? ? : U ? *?* ---------------------------------- ? ? ?x: A. ? : U ? ?*x*: *A*. *?* (using colour and styling to distinguish source/target, not entirely shown here) but abbreviations are still given for the translations with ? and U being implicit, so it doesn't look like there's a way around verbosity vs. abuse of notation here. In the end, the theorem is still stated as ? ? e : ? ? ?* ? e* : ?*, where e* ? *e* s.t. ? ? e : ? ? *e* and ?* ? *?* s.t. ? ? ? *?*, or using the ??? notation. On Sun, 22 May 2022 at 06:29, Stefan Monnier wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > I often write translations between PTS-style languages where the overall > structure of the translation can be represented by saying that an input > expression `e` is turned into an output `[e]` with a property like > > ? ? e : ? > => > [?] ? [e] : [?] > > Or some variant of it, very much like Boulier et al. did in "The next > 700 syntactical models of type theory". > > But often my translation function [?] needs a bit more info than that > provided by an expression. E.g. it may need to know the expression's > type or the typing context in which it was found. So what I end up > doing is to define my translation function as taking a typing derivation > as input while still returning a mere expression. > > Formally it means the above elegant property becomes: > > ? ? e : ? (which implies that ??. ? ? ? : Type?) > => > [?] ? [? ? e : ?] : [? ? ? : Type?] > > which is much less elegant and less friendly for the reader (I did > something like that for example in "Inductive types deconstructed: the > calculus of united constructions" and this was mentioned as an oddity > by one of the reviewers, for example). > > It also makes the presentation more verbose and harder to read, for > which the only way out I have found is to use cringe-worthy abuses of > notation where I might write [e] as a shorthand for [? ? e : ?] where > the ? and ? are presumed "obvious from context". > > Has anyone here faced similar issues? What's a better approach? > > > Stefan > > From andreasnuyts at gmail.com Mon May 23 04:44:19 2022 From: andreasnuyts at gmail.com (Andreas Nuyts) Date: Mon, 23 May 2022 10:44:19 +0200 Subject: [TYPES] Writing syntactic models with "full information" In-Reply-To: References: Message-ID: Dear Stefan, I would suggest the use of intrinsically typed syntax, defined as a quotient inductive-inductive type, see Altenkirch and Kaposi, Type theory in type theory using quotient inductive types https://urldefense.com/v3/__https://dl.acm.org/doi/abs/10.1145/2914770.2837638__;!!IBzWLUs!XatwrU-aKYd1XRa3nT193vk7ojHAJl14q2e1KUeemNUZzMN-wZ8bdlsnF09YA9guLUAsf2WsS7PI_7Yw7Jalw0amUAmD1UDAdw$ (and further work by either author). This way, omitting context and type is not cringe-worthy but formally justified in the sense that there is only a single (object-language) context and a single (object-language) type in which the (object-language) expression e is well-typed (in the metalanguage). I wouldn't recommend it as a strictly better approach, but it has its advantages. I don't know if formalization in a proof-assistant is a part of what you're doing. Altenkirch & Kaposi have an Agda formalization where they build quotient types using postulates & rewrite rules. Today, to my understanding, it should in principle be possible to instead do this in agda-cubical, although I don't think anyone has done it (and it sounds like a very major effort). FWIW, I have a formalization of multisorted algebraic theories and their categories of models in agda-cubical (currently using quite some termination pragmas rather than sized types) at https://urldefense.com/v3/__https://github.com/anuyts/ctx-alg/__;!!IBzWLUs!XatwrU-aKYd1XRa3nT193vk7ojHAJl14q2e1KUeemNUZzMN-wZ8bdlsnF09YA9guLUAsf2WsS7PI_7Yw7Jalw0amUAmobT5gJw$ Best regards, Andreas Nuyts On 21.05.22 03:16, Stefan Monnier wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > I often write translations between PTS-style languages where the overall > structure of the translation can be represented by saying that an input > expression `e` is turned into an output `[e]` with a property like > > ? ? e : ? > => > [?] ? [e] : [?] > > Or some variant of it, very much like Boulier et al. did in "The next > 700 syntactical models of type theory". > > But often my translation function [?] needs a bit more info than that > provided by an expression. E.g. it may need to know the expression's > type or the typing context in which it was found. So what I end up > doing is to define my translation function as taking a typing derivation > as input while still returning a mere expression. > > Formally it means the above elegant property becomes: > > ? ? e : ? (which implies that ??. ? ? ? : Type?) > => > [?] ? [? ? e : ?] : [? ? ? : Type?] > > which is much less elegant and less friendly for the reader (I did > something like that for example in "Inductive types deconstructed: the > calculus of united constructions" and this was mentioned as an oddity > by one of the reviewers, for example). > > It also makes the presentation more verbose and harder to read, for > which the only way out I have found is to use cringe-worthy abuses of > notation where I might write [e] as a shorthand for [? ? e : ?] where > the ? and ? are presumed "obvious from context". > > Has anyone here faced similar issues? What's a better approach? > > > Stefan > From monnier at iro.umontreal.ca Mon May 23 11:39:01 2022 From: monnier at iro.umontreal.ca (Stefan Monnier) Date: Mon, 23 May 2022 11:39:01 -0400 Subject: [TYPES] Writing syntactic models with "full information" In-Reply-To: (Andreas Nuyts's message of "Mon, 23 May 2022 10:44:19 +0200") References: Message-ID: Andreas Nuyts [2022-05-23 10:44:19] wrote: > I would suggest the use of intrinsically typed syntax, defined as a quotient > inductive-inductive type, see > Altenkirch and Kaposi, Type theory in type theory using quotient inductive > types > https://urldefense.com/v3/__https://dl.acm.org/doi/abs/10.1145/2914770.2837638__;!!IBzWLUs!UJ6ZI5x-rdMfJBtHWEi-LWwQgG_CQHpnLN_7JsHtojjYqW_ixR1U0HB8byOCf9q-KWc6aS-u-n6vuFFt9h5QDz1rXwWOzGcVyw$ > (and further work by either author). > This way, omitting context and type is not cringe-worthy but formally > justified in the sense that there is only a single (object-language) context > and a single (object-language) type in which the (object-language) > expression e is well-typed (in the metalanguage). I do tend to presume in my head that my terms are intrinsically typed, which is why I'm tempted to play fast and loose and abuse notations with things like [e] meaning [? ? e : ?], but at the same time I'm not completely comfortable relying on such a QIIT representation, because it doesn't seem sufficiently well established yet. E.g. I've never seen this used in an article. Obviously, there has to be a first for everything, but I'd rather not have to first give a bit of background on QIIT and show how to define my language using them before I can move on to the actual presentation of my translation. Also I often find myself working with languages that offer some form of impredicativity or some other feature for which I don't have a clear intuition whether I can assume that it is compatible with QIIT. Stefan From andreasnuyts at gmail.com Mon May 23 12:17:22 2022 From: andreasnuyts at gmail.com (Andreas Nuyts) Date: Mon, 23 May 2022 18:17:22 +0200 Subject: [TYPES] Writing syntactic models with "full information" In-Reply-To: References: Message-ID: <391a894f-6932-4338-d9b7-6c4756b0912f@gmail.com> I guess that is a justification to presume in one's head that context and type can be uniquely inferred by the reader :-) On 23.05.22 17:39, Stefan Monnier wrote: > I do tend to presume in my head that my terms are intrinsically typed, From kaposi.ambrus at gmail.com Tue May 24 11:52:10 2022 From: kaposi.ambrus at gmail.com (Ambrus Kaposi) Date: Tue, 24 May 2022 17:52:10 +0200 Subject: [TYPES] Writing syntactic models with "full information" In-Reply-To: References: Message-ID: On Mon, May 23, 2022 at 9:52 PM Stefan Monnier wrote: > > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Andreas Nuyts [2022-05-23 10:44:19] wrote: > > I would suggest the use of intrinsically typed syntax, defined as a quotient > > inductive-inductive type, see > > Altenkirch and Kaposi, Type theory in type theory using quotient inductive > > types > > https://urldefense.com/v3/__https://dl.acm.org/doi/abs/10.1145/2914770.2837638__;!!IBzWLUs!UJ6ZI5x-rdMfJBtHWEi-LWwQgG_CQHpnLN_7JsHtojjYqW_ixR1U0HB8byOCf9q-KWc6aS-u-n6vuFFt9h5QDz1rXwWOzGcVyw$ > > (and further work by either author). > > This way, omitting context and type is not cringe-worthy but formally > > justified in the sense that there is only a single (object-language) context > > and a single (object-language) type in which the (object-language) > > expression e is well-typed (in the metalanguage). > > I do tend to presume in my head that my terms are intrinsically typed, > which is why I'm tempted to play fast and loose and abuse notations with > things like [e] meaning [? ? e : ?], but at the same time I'm not > completely comfortable relying on such a QIIT representation, because it > doesn't seem sufficiently well established yet. > > E.g. I've never seen this used in an article. Here is a random list of papers that use QIIT syntax. Some people call it "well-typed/intrinsic syntax quotiented by conversion" or "initial model/algebra of the language". Thorsten Altenkirch, Ambrus Kaposi: Normalisation by Evaluation for Type Theory, in Type Theory. Log. Methods Comput. Sci. 13(4) (2017) https://urldefense.com/v3/__https://doi.org/10.23638/LMCS-13(4:1)2017__;!!IBzWLUs!RDvJg8Wh5lWFxZtFNvt0jkG968kLd1BJxx2Pu4Epfre8N1PRnKujIfjYYbJrmabdOK61SEgwmtf0yh3tB-wiqTXXHatHXXcjFgk$ Thorsten Altenkirch, Simon Boulier, Ambrus Kaposi, Nicolas Tabareau: Setoid Type Theory - A Syntactic Translation. MPC 2019: 155-196 https://urldefense.com/v3/__https://doi.org/10.1007/978-3-030-33636-3_7__;!!IBzWLUs!RDvJg8Wh5lWFxZtFNvt0jkG968kLd1BJxx2Pu4Epfre8N1PRnKujIfjYYbJrmabdOK61SEgwmtf0yh3tB-wiqTXXHatHLET6tTc$ Thierry Coquand: Canonicity and normalization for dependent type theory. Theor. Comput. Sci. 777: 184-191 (2019) https://urldefense.com/v3/__https://doi.org/10.1016/j.tcs.2019.01.015__;!!IBzWLUs!RDvJg8Wh5lWFxZtFNvt0jkG968kLd1BJxx2Pu4Epfre8N1PRnKujIfjYYbJrmabdOK61SEgwmtf0yh3tB-wiqTXXHatH_6H14yA$ Andreas Abel, Christian Sattler: Normalization by Evaluation for Call-By-Push-Value and Polarized Lambda Calculus. PPDP 2019: 3:1-3:12 https://urldefense.com/v3/__https://doi.org/10.1145/3354166.3354168__;!!IBzWLUs!RDvJg8Wh5lWFxZtFNvt0jkG968kLd1BJxx2Pu4Epfre8N1PRnKujIfjYYbJrmabdOK61SEgwmtf0yh3tB-wiqTXXHatHNNF55NE$ Andr?s Kov?cs. Elaboration with first-class implicit function types. Proc. ACM Program. Lang. 4(ICFP): 101:1-101:29 (2020) https://urldefense.com/v3/__https://doi.org/10.1145/3408983__;!!IBzWLUs!RDvJg8Wh5lWFxZtFNvt0jkG968kLd1BJxx2Pu4Epfre8N1PRnKujIfjYYbJrmabdOK61SEgwmtf0yh3tB-wiqTXXHatHvgrE5ws$ Jonathan Sterling, Carlo Angiuli: Normalization for Cubical Type Theory. LICS 2021: 1-15 https://urldefense.com/v3/__https://doi.org/10.1109/LICS52264.2021.9470719__;!!IBzWLUs!RDvJg8Wh5lWFxZtFNvt0jkG968kLd1BJxx2Pu4Epfre8N1PRnKujIfjYYbJrmabdOK61SEgwmtf0yh3tB-wiqTXXHatHDJJWemc$ From fdhzs2010 at hotmail.com Tue May 24 20:07:38 2022 From: fdhzs2010 at hotmail.com (Jason Hu) Date: Wed, 25 May 2022 00:07:38 +0000 Subject: [TYPES] Writing syntactic models with "full information" In-Reply-To: References: Message-ID: I don?t know how intrinstically typed formulation can be used to express universes, at least I have not seen one. With intrinsic formulation, one must index an Exp with a context and a type, but with MLTT-style dependent types, a type is also an Exp, which requires an Exp to be indexed by an Exp. Is it then possible to tackle it by Tarski-style universes, where types and terms are separated? It sounds to me intrinsic formulation conflicts with Russell-style universes. In my opinion, I much prefer extrinsic formulation, where we have pre-syntax and typing judgments there to give semantics later. This way avoids many type-level gymnastics that often people do not want to handle. From: Stefan Monnier Sent: Monday, May 23, 2022 3:51 PM To: Andreas Nuyts Cc: types-list at lists.seas.upenn.edu Subject: Re: [TYPES] Writing syntactic models with "full information" [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] Andreas Nuyts [2022-05-23 10:44:19] wrote: > I would suggest the use of intrinsically typed syntax, defined as a quotient > inductive-inductive type, see > Altenkirch and Kaposi, Type theory in type theory using quotient inductive > types > https://urldefense.com/v3/__https://dl.acm.org/doi/abs/10.1145/2914770.2837638__;!!IBzWLUs!UJ6ZI5x-rdMfJBtHWEi-LWwQgG_CQHpnLN_7JsHtojjYqW_ixR1U0HB8byOCf9q-KWc6aS-u-n6vuFFt9h5QDz1rXwWOzGcVyw$ > (and further work by either author). > This way, omitting context and type is not cringe-worthy but formally > justified in the sense that there is only a single (object-language) context > and a single (object-language) type in which the (object-language) > expression e is well-typed (in the metalanguage). I do tend to presume in my head that my terms are intrinsically typed, which is why I'm tempted to play fast and loose and abuse notations with things like [e] meaning [? ? e : ?], but at the same time I'm not completely comfortable relying on such a QIIT representation, because it doesn't seem sufficiently well established yet. E.g. I've never seen this used in an article. Obviously, there has to be a first for everything, but I'd rather not have to first give a bit of background on QIIT and show how to define my language using them before I can move on to the actual presentation of my translation. Also I often find myself working with languages that offer some form of impredicativity or some other feature for which I don't have a clear intuition whether I can assume that it is compatible with QIIT. Stefan From jon at jonmsterling.com Wed May 25 04:38:18 2022 From: jon at jonmsterling.com (Jon Sterling) Date: Wed, 25 May 2022 10:38:18 +0200 Subject: [TYPES] Writing syntactic models with "full information" In-Reply-To: References: Message-ID: <7AFED7F5-AAB1-4DDB-87AD-3B2F86E28F74@jonmsterling.com> I do not know why you think that the intrinsically typed formulation cannot be used to express universes... I haven't specifically done so using QIITs, but using a variety of other analogous frameworks (generalized algebraic theories, sketched LCCCs / extensional logical framework); there are a dozen different ways to present intrinsically typed syntax, but they are all based on the same idea. There have been probably a ton of examples of universes in intrinsically typed frameworks by now, but let me give just a couple examples: - Nordstr?m, Peterssen, Smith. Programming in Martin-L?f's Type Theory (https://urldefense.com/v3/__http://www.cse.chalmers.se/research/group/logic/book/__;!!IBzWLUs!XNAIW9QIDrRGxrfUK2_hVSIzBwo8n3TsirgM0o7tArAE_QstUpr82ip9qJsDZX3e5CjkmwuGSPzLLeaeTxmf7UrU3NA$ ). This expresses universes inside Martin-L?f's logical framework, an informal framework for intrinsically typed syntax. This is very old, but proves there is no problem with universes in a logical framework. - Sterling. Algebraic type theory and universe hierarchies (https://urldefense.com/v3/__https://arxiv.org/pdf/1902.08848.pdf__;!!IBzWLUs!XNAIW9QIDrRGxrfUK2_hVSIzBwo8n3TsirgM0o7tArAE_QstUpr82ip9qJsDZX3e5CjkmwuGSPzLLeaeTxmfsfwSA4s$ ). This was a pretty outdated one by myself in the language of "generalized algebraic theories", I have no doubt there are better examples now, but I include it for completeness. - Kovacs. Generalized Universe Hierarchies and First-Class Universe Levels (https://urldefense.com/v3/__https://arxiv.org/abs/2103.00223__;!!IBzWLUs!XNAIW9QIDrRGxrfUK2_hVSIzBwo8n3TsirgM0o7tArAE_QstUpr82ip9qJsDZX3e5CjkmwuGSPzLLeaeTxmfayIoNos$ ). - Sterling, Angiuli, Gratzer. Cubical Syntax for Reflection-Free Extensional Equality (https://urldefense.com/v3/__https://www.jonmsterling.com/abstracts.html*sterling-angiuli-gratzer:2019__;Iw!!IBzWLUs!XNAIW9QIDrRGxrfUK2_hVSIzBwo8n3TsirgM0o7tArAE_QstUpr82ip9qJsDZX3e5CjkmwuGSPzLLeaeTxmfKciIT-Y$ ). This uses the language of generalized algebraic theories. - Sterling, Angiuli, Gratzer. A Cubical Language for Bishop Sets (https://urldefense.com/v3/__https://www.jonmsterling.com/abstracts.html*sterling-angiuli-gratzer:2022__;Iw!!IBzWLUs!XNAIW9QIDrRGxrfUK2_hVSIzBwo8n3TsirgM0o7tArAE_QstUpr82ip9qJsDZX3e5CjkmwuGSPzLLeaeTxmfwLss2XI$ ). This reformulates the previous paper in Taichi Uemura's framework for intrinsically typed syntax. - Sterling, Harper. Logical Relations as Types (https://urldefense.com/v3/__https://www.jonmsterling.com/abstracts.html*sterling-harper:2021__;Iw!!IBzWLUs!XNAIW9QIDrRGxrfUK2_hVSIzBwo8n3TsirgM0o7tArAE_QstUpr82ip9qJsDZX3e5CjkmwuGSPzLLeaeTxmfuNOBo4U$ ). This expresses universes in an extensional logical framework (formally, it is generating the free LCCC on some generators). - Sterling. First Steps in Synthetic Tait Computability (https://urldefense.com/v3/__https://www.jonmsterling.com/abstracts.html*sterling:2021:thesis__;Iw!!IBzWLUs!XNAIW9QIDrRGxrfUK2_hVSIzBwo8n3TsirgM0o7tArAE_QstUpr82ip9qJsDZX3e5CjkmwuGSPzLLeaeTxmfRBkQisA$ ). This uses the same methods as Logical Relations as Types. No doubt there is also a dozen papers by Ambrus Kaposi and Thorsten Altenkirch that do the same thing... To return to your concerns, it is true that there are things that happen in "syntax" that are not included in these frameworks; these are things like the idea of one element inhabiting multiple types. But these behaviors are **always** understood today as being shorthands for some kind of coercion, and coercions are expressible in these intrinsically typed frameworks. I hope these references help, Jon On Wed, May 25, 2022, at 2:07 AM, Jason Hu wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > I don?t know how intrinstically typed formulation can be used to > express universes, at least I have not seen one. > > With intrinsic formulation, one must index an Exp with a context and a > type, but with MLTT-style dependent types, a type is also an Exp, which > requires an Exp to be indexed by an Exp. > > Is it then possible to tackle it by Tarski-style universes, where types > and terms are separated? It sounds to me intrinsic formulation > conflicts with Russell-style universes. > > In my opinion, I much prefer extrinsic formulation, where we have > pre-syntax and typing judgments there to give semantics later. This way > avoids many type-level gymnastics that often people do not want to > handle. > > > From: Stefan Monnier > Sent: Monday, May 23, 2022 3:51 PM > To: Andreas Nuyts > Cc: types-list at lists.seas.upenn.edu > Subject: Re: [TYPES] Writing syntactic models with "full information" > > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Andreas Nuyts [2022-05-23 10:44:19] wrote: >> I would suggest the use of intrinsically typed syntax, defined as a quotient >> inductive-inductive type, see >> Altenkirch and Kaposi, Type theory in type theory using quotient inductive >> types >> https://urldefense.com/v3/__https://dl.acm.org/doi/abs/10.1145/2914770.2837638__;!!IBzWLUs!UJ6ZI5x-rdMfJBtHWEi-LWwQgG_CQHpnLN_7JsHtojjYqW_ixR1U0HB8byOCf9q-KWc6aS-u-n6vuFFt9h5QDz1rXwWOzGcVyw$ >> (and further work by either author). >> This way, omitting context and type is not cringe-worthy but formally >> justified in the sense that there is only a single (object-language) context >> and a single (object-language) type in which the (object-language) >> expression e is well-typed (in the metalanguage). > > I do tend to presume in my head that my terms are intrinsically typed, > which is why I'm tempted to play fast and loose and abuse notations with > things like [e] meaning [? ? e : ?], but at the same time I'm not > completely comfortable relying on such a QIIT representation, because it > doesn't seem sufficiently well established yet. > > E.g. I've never seen this used in an article. Obviously, there has to > be a first for everything, but I'd rather not have to first give a bit of > background on QIIT and show how to define my language using them before > I can move on to the actual presentation of my translation. > > Also I often find myself working with languages that offer some form of > impredicativity or some other feature for which I don't have a clear > intuition whether I can assume that it is compatible with QIIT. > > > Stefan From fdhzs2010 at hotmail.com Wed May 25 09:27:55 2022 From: fdhzs2010 at hotmail.com (Jason Hu) Date: Wed, 25 May 2022 13:27:55 +0000 Subject: [TYPES] Writing syntactic models with "full information" In-Reply-To: References: Message-ID: Hi Thorsten, I value your and your students? work because I looked into it and learned how things can be done intrinsically. IMO, intrinsic and extrinsic styles are only distinguished by what phase semantics are given in. I don?t think both historically and technically, either style is superior to or more proper than the other. To me, it?s like stepping forward with the left foot or the right foot first. Nevertheless, I do have preference, not to mention I have greatly benefited from the ?stone axe? recently. So there is nothing depressing here, more like a matter of choice and taste. From: Thorsten Altenkirch Sent: Wednesday, May 25, 2022 5:14 AM To: Jason Hu; Stefan Monnier; Andreas Nuyts Cc: types-list at lists.seas.upenn.edu Subject: Re: [TYPES] Writing syntactic models with "full information" From: Types-list on behalf of Jason Hu Date: Wednesday, 25 May 2022 at 09:58 To: Stefan Monnier , Andreas Nuyts Cc: types-list at lists.seas.upenn.edu Subject: Re: [TYPES] Writing syntactic models with "full information" [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] I don?t know how intrinstically typed formulation can be used to express universes, at least I have not seen one. There is no problem and we have done it many times U : Ty G El : Tm G U -> Ty G With intrinsic formulation, one must index an Exp with a context and a type, but with MLTT-style dependent types, a type is also an Exp, which requires an Exp to be indexed by an Exp. Is it then possible to tackle it by Tarski-style universes, where types and terms are separated? It sounds to me intrinsic formulation conflicts with Russell-style universes. See our forthcoming TYPES talk (presented by Artem Shinkarov). In my opinion, I much prefer extrinsic formulation, where we have pre-syntax and typing judgments there to give semantics later. This way avoids many type-level gymnastics that often people do not want to handle. You have to perform lots of Gymnastics when you are stuck in the last millennium formulation of Type Theory. The intrinsic syntax of type theory are just the initial categories with families, syntax and semantics fit perfectly. I have started with the extrinsic formulation of type theory (see my PhD), beta-reduction and single-place substitution. In each instance we learnt how to do things properly: intrinsic, equality, parallel substitution. And then you come and say: ?I prefer the stone axe?. It is depressing. Thorsten From: Stefan Monnier Sent: Monday, May 23, 2022 3:51 PM To: Andreas Nuyts Cc: types-list at lists.seas.upenn.edu Subject: Re: [TYPES] Writing syntactic models with "full information" [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] Andreas Nuyts [2022-05-23 10:44:19] wrote: > I would suggest the use of intrinsically typed syntax, defined as a quotient > inductive-inductive type, see > Altenkirch and Kaposi, Type theory in type theory using quotient inductive > types > https://urldefense.com/v3/__https://dl.acm.org/doi/abs/10.1145/2914770.2837638__;!!IBzWLUs!UJ6ZI5x-rdMfJBtHWEi-LWwQgG_CQHpnLN_7JsHtojjYqW_ixR1U0HB8byOCf9q-KWc6aS-u-n6vuFFt9h5QDz1rXwWOzGcVyw$ > (and further work by either author). > This way, omitting context and type is not cringe-worthy but formally > justified in the sense that there is only a single (object-language) context > and a single (object-language) type in which the (object-language) > expression e is well-typed (in the metalanguage). I do tend to presume in my head that my terms are intrinsically typed, which is why I'm tempted to play fast and loose and abuse notations with things like [e] meaning [? ? e : ?], but at the same time I'm not completely comfortable relying on such a QIIT representation, because it doesn't seem sufficiently well established yet. E.g. I've never seen this used in an article. Obviously, there has to be a first for everything, but I'd rather not have to first give a bit of background on QIIT and show how to define my language using them before I can move on to the actual presentation of my translation. Also I often find myself working with languages that offer some form of impredicativity or some other feature for which I don't have a clear intuition whether I can assume that it is compatible with QIIT. Stefan This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law. From P.B.Levy at cs.bham.ac.uk Wed May 25 12:09:27 2022 From: P.B.Levy at cs.bham.ac.uk (Paul Blain Levy) Date: Wed, 25 May 2022 17:09:27 +0100 Subject: [TYPES] Writing syntactic models with "full information" In-Reply-To: References: Message-ID: Dear Stefan, Like you, I write [[ e ]] as an informal shorthand for [[ Gamma |- e:A ]], but this is not really correct. For example, in simply typed lambda-calculus with zero type and boolean type, we have [[ x:0 |- true:bool ]] = [[ x:0 |- false:bool ]] but not [[ |- true:bool ]] = [[ |- false:bool ]] Best, Paul > On 21 May 2022, at 02:16, monnier at iro.umontreal.ca wrote: > > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > I often write translations between PTS-style languages where the overall > structure of the translation can be represented by saying that an input > expression `e` is turned into an output `[e]` with a property like > > ? ? e : ? > => > [?] ? [e] : [?] > > Or some variant of it, very much like Boulier et al. did in "The next > 700 syntactical models of type theory". > > But often my translation function [?] needs a bit more info than that > provided by an expression. E.g. it may need to know the expression's > type or the typing context in which it was found. So what I end up > doing is to define my translation function as taking a typing derivation > as input while still returning a mere expression. > > Formally it means the above elegant property becomes: > > ? ? e : ? (which implies that ??. ? ? ? : Type?) > => > [?] ? [? ? e : ?] : [? ? ? : Type?] > > which is much less elegant and less friendly for the reader (I did > something like that for example in "Inductive types deconstructed: the > calculus of united constructions" and this was mentioned as an oddity > by one of the reviewers, for example). > > It also makes the presentation more verbose and harder to read, for > which the only way out I have found is to use cringe-worthy abuses of > notation where I might write [e] as a shorthand for [? ? e : ?] where > the ? and ? are presumed "obvious from context". > > Has anyone here faced similar issues? What's a better approach? > > > Stefan > From xyheme at gmail.com Fri May 27 03:20:29 2022 From: xyheme at gmail.com (xieyuheng) Date: Fri, 27 May 2022 15:20:29 +0800 Subject: [TYPES] A Paper: "Type System as Homomorphism between Monoids" Message-ID: Link to the paper: https://urldefense.com/v3/__https://readonly.link/articles/xieyuheng/xieyuheng/-/papers/publish/type-system-as-homomorphism-between-monoids.md__;!!IBzWLUs!QDKONs89nYQk1pdWyJwpctfD9aMo_yPCUbkQ-U-7OiW42F8IB6h8ki4UXNfwRoD7DT2XmvxPBKuSGjxmf2FykWdZHg$ **Abstract** We demonstrate how to view a type system as a homomorphism between two monoids, where the space of types is monoid, the space of terms is also a monoid, and the homomorphism is the `infer` function of the type system. We use a concrete example to demonstrate this idea, in our example the space of types is _linear logic propositions_, and the space of terms is a _concatenative programming language_ (like Forth and Joy). Some key points of our demonstration: - Negation of linear logic should NOT be interpreted as "implying false", but be interpreted as a type of _linear assignment_ (thus constructive). - Linear logic additive connectives can be interpreted without concurrency. - Type errors will be captured by a special `Error` element. From xyheme at gmail.com Fri May 27 03:21:33 2022 From: xyheme at gmail.com (xieyuheng) Date: Fri, 27 May 2022 15:21:33 +0800 Subject: [TYPES] A new dependently typed language: Cicada Language Message-ID: Link to the project homepage: https://urldefense.com/v3/__https://cicada-lang.org__;!!IBzWLUs!WUz_8y3AyuLRoPc06TbMyn8QDs93jw-zb-Sts9CBUuCliEeQPo0pF-B9s2ib2alHcPmj_OxbISzi-C5krFc5GD3IWA$ Link to the manual of the language: https://urldefense.com/v3/__https://readonly.link/manuals/cicada-lang/cicada__;!!IBzWLUs!WUz_8y3AyuLRoPc06TbMyn8QDs93jw-zb-Sts9CBUuCliEeQPo0pF-B9s2ib2alHcPmj_OxbISzi-C5krFdhERIIpg$ The aim of cicada project is to help people understand that developing software and developing mathematics are increasingly the same kind of activity, and people who practice these developments can learn from each other, and help each other in very good ways. From fangyi.zhou15 at imperial.ac.uk Thu Jun 9 08:31:33 2022 From: fangyi.zhou15 at imperial.ac.uk (Fangyi Zhou) Date: Thu, 09 Jun 2022 13:31:33 +0100 Subject: [TYPES] What is the term after reduction called? Message-ID: <76cc3048bcff055661c084cc3ff9dde3436dd674.camel@imperial.ac.uk> Dear TYPES mailing list Let M -> N. It appears to me that the terminology for terms before reduction (M) is sometimes called a reducible expression (redex), although the concept of redex seems to be more general than that. Is there an agreed terminology for the term after reduction (N)? The wikipedia page for lambda calculus (without giving any sources) calls the expression to which a redex reduces to a 'reduct', but I've seen other words used such as 'reductum'. Apologies if the question is silly. Best, Fangyi -- Fangyi Zhou (Pronouns: they/them) PhD Student Mobility Reading Group Department of Computing Imperial College London From hendrik at topoi.pooq.com Thu Jun 9 11:10:21 2022 From: hendrik at topoi.pooq.com (Hendrik Boom) Date: Thu, 9 Jun 2022 11:10:21 -0400 Subject: [TYPES] What is the term after reduction called? In-Reply-To: <76cc3048bcff055661c084cc3ff9dde3436dd674.camel@imperial.ac.uk> References: <76cc3048bcff055661c084cc3ff9dde3436dd674.camel@imperial.ac.uk> Message-ID: <20220609151021.GA10454@topoi.pooq.com> On Thu, Jun 09, 2022 at 01:31:33PM +0100, Fangyi Zhou wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Dear TYPES mailing list > > Let M -> N. > > It appears to me that the terminology for terms before reduction (M) is > sometimes called a reducible expression (redex), although the concept of redex > seems to be more general than that. The word that came to mind when I had just read the title of this post was 'reduct'. > > Is there an agreed terminology for the term after reduction (N)? > The wikipedia page for lambda calculus (without giving any sources) calls the > expression to which a redex reduces to a 'reduct', but I've seen other words > used such as 'reductum'. I suspect that is for writers that use latin to give their writing a classical sound. -- hendrik > > Apologies if the question is silly. > > Best, > Fangyi > > -- > Fangyi Zhou (Pronouns: they/them) > PhD Student > Mobility Reading Group > Department of Computing > Imperial College London > From hindley at waitrose.com Thu Jun 9 12:29:09 2022 From: hindley at waitrose.com (J. R. Hindley) Date: Thu, 9 Jun 2022 17:29:09 +0100 Subject: [TYPES] What is the term after reduction called? In-Reply-To: <76cc3048bcff055661c084cc3ff9dde3436dd674.camel@imperial.ac.uk> References: <76cc3048bcff055661c084cc3ff9dde3436dd674.camel@imperial.ac.uk> Message-ID: Dear Fangyi Zhou, The name "redex" was invented by Haskell Curry, see Section 3D5 in the book "Combinatory Logic" by Curry and Feys 1958. He called the result of contracting a redex "the contractum of the redex". > Is there an agreed terminology for the term after reduction (N)? No, I think there is no agreed terminology. Perhaps the reason is that (in lambda-calculus) every term can be a reductum or contractum, but not every term can be a redex. For example, let T be any term; if we choose R to be the redex (\x.x)T, then R contracts to T, so T is a reductum. Good luck, Roger Hindley From wjb at williamjbowman.com Thu Jun 9 13:19:43 2022 From: wjb at williamjbowman.com (William J. Bowman) Date: Thu, 9 Jun 2022 10:19:43 -0700 Subject: [TYPES] What is the term after reduction called? In-Reply-To: <76cc3048bcff055661c084cc3ff9dde3436dd674.camel@imperial.ac.uk> References: <76cc3048bcff055661c084cc3ff9dde3436dd674.camel@imperial.ac.uk> Message-ID: I've seen "reduct", but also "contractum". See e.g. "Semantics Engineering with PLT Redex". As with much terminology and notation, I doubt you will find one true answer. -- William J. Bowman On Thu, Jun 09, 2022 at 01:31:33PM +0100, Fangyi Zhou wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Dear TYPES mailing list > > Let M -> N. > > It appears to me that the terminology for terms before reduction (M) is > sometimes called a reducible expression (redex), although the concept of redex > seems to be more general than that. > > Is there an agreed terminology for the term after reduction (N)? > The wikipedia page for lambda calculus (without giving any sources) calls the > expression to which a redex reduces to a 'reduct', but I've seen other words > used such as 'reductum'. > > Apologies if the question is silly. > > Best, > Fangyi > > -- > Fangyi Zhou (Pronouns: they/them) > PhD Student > Mobility Reading Group > Department of Computing > Imperial College London > From fritz at henglein.com Sat Jun 11 05:09:30 2022 From: fritz at henglein.com (Fritz Henglein) Date: Sat, 11 Jun 2022 11:09:30 +0200 Subject: [TYPES] What is the term after reduction called? In-Reply-To: <76cc3048bcff055661c084cc3ff9dde3436dd674.camel@imperial.ac.uk> References: <76cc3048bcff055661c084cc3ff9dde3436dd674.camel@imperial.ac.uk> Message-ID: Commonly 'reduct' is used, which is English and derived from the Latin 'reductum'. But since Latin is arguably a conditio sine qua non of erudite discourse, 'reductum' is clearly an option. (Writing the remainder of one's paper in Latin may be a challenge and not an H-index friendly strategy, though. It hasn't been done much since Gauss's Disquisitiones Arithmeticae.) On Thu, Jun 9, 2022 at 2:38 PM Fangyi Zhou wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > Dear TYPES mailing list > > Let M -> N. > > It appears to me that the terminology for terms before reduction (M) is > sometimes called a reducible expression (redex), although the concept of > redex > seems to be more general than that. > > Is there an agreed terminology for the term after reduction (N)? > The wikipedia page for lambda calculus (without giving any sources) calls > the > expression to which a redex reduces to a 'reduct', but I've seen other > words > used such as 'reductum'. > > Apologies if the question is silly. > > Best, > Fangyi > > -- > Fangyi Zhou (Pronouns: they/them) > PhD Student > Mobility Reading Group > Department of Computing > Imperial College London > > From jon at jonmsterling.com Sun Jun 12 14:42:58 2022 From: jon at jonmsterling.com (Jon Sterling) Date: Sun, 12 Jun 2022 20:42:58 +0200 Subject: [TYPES] What is the term after reduction called? In-Reply-To: <20220609151021.GA10454@topoi.pooq.com> References: <76cc3048bcff055661c084cc3ff9dde3436dd674.camel@imperial.ac.uk> <20220609151021.GA10454@topoi.pooq.com> Message-ID: 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, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > On Thu, Jun 09, 2022 at 01:31:33PM +0100, Fangyi Zhou wrote: >> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] >> >> Dear TYPES mailing list >> >> Let M -> N. >> >> It appears to me that the terminology for terms before reduction (M) is >> sometimes called a reducible expression (redex), although the concept of redex >> seems to be more general than that. > > The word that came to mind when I had just read the title of this post > was 'reduct'. > >> >> Is there an agreed terminology for the term after reduction (N)? >> The wikipedia page for lambda calculus (without giving any sources) calls the >> expression to which a redex reduces to a 'reduct', but I've seen other words >> used such as 'reductum'. > > I suspect that is for writers that use latin to give their writing a > classical sound. > > -- hendrik > >> >> Apologies if the question is silly. >> >> Best, >> Fangyi >> >> -- >> Fangyi Zhou (Pronouns: they/them) >> PhD Student >> Mobility Reading Group >> Department of Computing >> Imperial College London >> From aaronngray.lists at gmail.com Fri Jun 17 03:40:32 2022 From: aaronngray.lists at gmail.com (Aaron Gray) Date: Fri, 17 Jun 2022 08:40:32 +0100 Subject: [TYPES] subtyping of mutually recursive algebraic data types Message-ID: I am interested if there is any work on the subtyping of mutually recursive algebraic data types. I am wanting an algorithm for purposes of implementing an object oriented programming language with ADT's which lower onto a virtual class implementation which can support mutually recursive behavior, but need the typ checking and inference at the ADT level. Theres a number of papers and projects in this area I have came across but none of them actually tackle algebraic data types properly let alone mutually recursive ones. A number inspired by Stephen Dolan's PhD Thesis and MLsub, his implementation. - Practical Subtyping for Curry-Style Languages by Rodolphe Lepigre and Christophe Raffalli - subml - https://urldefense.com/v3/__https://github.com/rlepigre/subml__;!!IBzWLUs!ROzY30gWHR0LPvTTZLo_Ep7ErCu0LhX2jrPKbFJ9uhVgSSx659leOfq_pNrPSAGgLExea89yhX9iVce14nA987dFVoNzXhSpE6cZJg$ - The Simple Essence of Algebraic Subtyping, Lionel Parreaux and simple-sub implementation - https://urldefense.com/v3/__https://github.com/LPTK/simple-sub__;!!IBzWLUs!ROzY30gWHR0LPvTTZLo_Ep7ErCu0LhX2jrPKbFJ9uhVgSSx659leOfq_pNrPSAGgLExea89yhX9iVce14nA987dFVoNzXhS4dNcEiw$ - A Mechanical Soundness Proof for Subtyping Over Recursive Types Timothy Jones David J. Pearce - https://urldefense.com/v3/__https://github.com/zmthy/recursive-types__;!!IBzWLUs!ROzY30gWHR0LPvTTZLo_Ep7ErCu0LhX2jrPKbFJ9uhVgSSx659leOfq_pNrPSAGgLExea89yhX9iVce14nA987dFVoNzXhRACugkxw$ None of these seem to deal with mutually recursive data types. I am interested in the papproach of using codata/coinduction and coalgebras and possibly bisimulation in order to deal with the mutually recursive nature of real world mutually recursive algebraic data types like for instance AST's of real world complex computer languages. Any projects, papers, thoughts, or implementations would be of interest. Regards, Aaron From sheldon at alum.mit.edu Fri Jun 17 12:59:56 2022 From: sheldon at alum.mit.edu (Mark Sheldon) Date: Fri, 17 Jun 2022 12:59:56 -0400 Subject: [TYPES] subtyping of mutually recursive algebraic data types In-Reply-To: References: Message-ID: We deal with this topic in our book, Design Concepts in Programming Languages (https://urldefense.com/v3/__https://mitpress.mit.edu/books/design-concepts-programming-languages__;!!IBzWLUs!UeVFMEtYt8ckfm-t6zKFlGaiVtH17ToAFSrNnbbzCRByAVfFL8Wqo1XYb-zSLszkXmc_8vnfzc_F6OJH3va6LwopH_nYGc2Q$ ). See Chapter 12. There is a section on ?Subtyping of Recursive Types on pages 706?707, Here are relevant references given in the Notes section of Chapter 12 on page 767: Kozen, Palsberg, Schwartzbach. Efficent recursive subtyping. POPL 93. Gapayev, Levin, Pierce. Recursive subtyping revealed. ICFP 00. Pierce. Types and Programming Languages. MIT Press. 2002. Chapter 12. I hope this is useful! -Mark Mark A. Sheldon Associate Teaching Professor Department of Computer Science Tufts University > On 17Jun, 2022, at 03:40, Aaron Gray wrote: > > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > I am interested if there is any work on the subtyping of mutually > recursive algebraic data types. I am wanting an algorithm for purposes > of implementing an object oriented programming language with ADT's > which lower onto a virtual class implementation which can support > mutually recursive behavior, but need the typ checking and inference > at the ADT level. > > Theres a number of papers and projects in this area I have came across > but none of them actually tackle algebraic data types properly let > alone mutually recursive ones. > > A number inspired by Stephen Dolan's PhD Thesis and MLsub, his implementation. > > - Practical Subtyping for Curry-Style Languages by Rodolphe Lepigre > and Christophe Raffalli - subml - https://urldefense.com/v3/__https://github.com/rlepigre/subml__;!!IBzWLUs!ROzY30gWHR0LPvTTZLo_Ep7ErCu0LhX2jrPKbFJ9uhVgSSx659leOfq_pNrPSAGgLExea89yhX9iVce14nA987dFVoNzXhSpE6cZJg$ > - The Simple Essence of Algebraic Subtyping, Lionel Parreaux and > simple-sub implementation - https://urldefense.com/v3/__https://github.com/LPTK/simple-sub__;!!IBzWLUs!ROzY30gWHR0LPvTTZLo_Ep7ErCu0LhX2jrPKbFJ9uhVgSSx659leOfq_pNrPSAGgLExea89yhX9iVce14nA987dFVoNzXhS4dNcEiw$ > - A Mechanical Soundness Proof for Subtyping Over Recursive Types > Timothy Jones David J. Pearce - > https://urldefense.com/v3/__https://github.com/zmthy/recursive-types__;!!IBzWLUs!ROzY30gWHR0LPvTTZLo_Ep7ErCu0LhX2jrPKbFJ9uhVgSSx659leOfq_pNrPSAGgLExea89yhX9iVce14nA987dFVoNzXhRACugkxw$ > > None of these seem to deal with mutually recursive data types. > > I am interested in the papproach of using codata/coinduction and > coalgebras and possibly bisimulation in order to deal with the > mutually recursive nature of real world mutually recursive algebraic > data types like for instance AST's of real world complex computer > languages. > > Any projects, papers, thoughts, or implementations would be of interest. > > Regards, > > Aaron From fp at cs.cmu.edu Sat Jun 18 08:41:58 2022 From: fp at cs.cmu.edu (Frank Pfenning) Date: Sat, 18 Jun 2022 06:41:58 -0600 Subject: [TYPES] subtyping of mutually recursive algebraic data types In-Reply-To: References: Message-ID: You might find our recent ESOP paper relevant: Zeeshan Lakhani, Ankush Das, Henry DeYoung, Andreia Mordido, Frank Pfenning: Polarized Subtyping. ESOP 2022: 431-461 https://urldefense.com/v3/__https://link.springer.com/chapter/10.1007/978-3-030-99336-8_16__;!!IBzWLUs!QrMnoLw8qFRxtzf2zu5w8Gc14aO6rhn_cCBMv4Q0dczTVPBFrRikSVu7fiARjhLIovnBm3oBBgYJ2dYwzqkdvV8$ There are some further references in that paper in the related work section. A version with polymorphism, but without explicit polarization (essentially: all types are interpreted coinductively because they are session types) can be found in Ankush Das, Henry DeYoung, Andreia Mordido, Frank Pfenning: Subtyping on Nested Polymorphic Session Types. CoRR abs/2103.15193 (2021) https://urldefense.com/v3/__https://arxiv.org/abs/2103.15193__;!!IBzWLUs!QrMnoLw8qFRxtzf2zu5w8Gc14aO6rhn_cCBMv4Q0dczTVPBFrRikSVu7fiARjhLIovnBm3oBBgYJ2dYwMw8Y7mY$ There we show that a natural formulation of the problem in the presence of polymorphism is undecidable, but also give an algorithm that has performed well for us in practice. - Frank On Fri, Jun 17, 2022 at 9:11 AM Aaron Gray wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > I am interested if there is any work on the subtyping of mutually > recursive algebraic data types. I am wanting an algorithm for purposes > of implementing an object oriented programming language with ADT's > which lower onto a virtual class implementation which can support > mutually recursive behavior, but need the typ checking and inference > at the ADT level. > > Theres a number of papers and projects in this area I have came across > but none of them actually tackle algebraic data types properly let > alone mutually recursive ones. > > A number inspired by Stephen Dolan's PhD Thesis and MLsub, his > implementation. > > - Practical Subtyping for Curry-Style Languages by Rodolphe Lepigre > and Christophe Raffalli - subml - > https://urldefense.com/v3/__https://github.com/rlepigre/subml__;!!IBzWLUs!ROzY30gWHR0LPvTTZLo_Ep7ErCu0LhX2jrPKbFJ9uhVgSSx659leOfq_pNrPSAGgLExea89yhX9iVce14nA987dFVoNzXhSpE6cZJg$ > - The Simple Essence of Algebraic Subtyping, Lionel Parreaux and > simple-sub implementation - > https://urldefense.com/v3/__https://github.com/LPTK/simple-sub__;!!IBzWLUs!ROzY30gWHR0LPvTTZLo_Ep7ErCu0LhX2jrPKbFJ9uhVgSSx659leOfq_pNrPSAGgLExea89yhX9iVce14nA987dFVoNzXhS4dNcEiw$ > - A Mechanical Soundness Proof for Subtyping Over Recursive Types > Timothy Jones David J. Pearce - > > https://urldefense.com/v3/__https://github.com/zmthy/recursive-types__;!!IBzWLUs!ROzY30gWHR0LPvTTZLo_Ep7ErCu0LhX2jrPKbFJ9uhVgSSx659leOfq_pNrPSAGgLExea89yhX9iVce14nA987dFVoNzXhRACugkxw$ > > None of these seem to deal with mutually recursive data types. > > I am interested in the papproach of using codata/coinduction and > coalgebras and possibly bisimulation in order to deal with the > mutually recursive nature of real world mutually recursive algebraic > data types like for instance AST's of real world complex computer > languages. > > Any projects, papers, thoughts, or implementations would be of interest. > > Regards, > > Aaron > -- Frank Pfenning, Professor Computer Science Department Carnegie Mellon University Pittsburgh, PA 15213-3891 https://urldefense.com/v3/__http://www.cs.cmu.edu/*fp__;fg!!IBzWLUs!QrMnoLw8qFRxtzf2zu5w8Gc14aO6rhn_cCBMv4Q0dczTVPBFrRikSVu7fiARjhLIovnBm3oBBgYJ2dYwrgSsDME$ +1 412 268-6343 GHC 6017 From gc at irif.fr Sat Jun 18 18:07:15 2022 From: gc at irif.fr (Giuseppe Castagna) Date: Sun, 19 Jun 2022 00:07:15 +0200 Subject: [TYPES] subtyping of mutually recursive algebraic data types In-Reply-To: References: Message-ID: <380ead85-e0a1-2d16-0226-79ddfeae5e81@irif.fr> In our ICFP 16 Paper /Set-Theoretic Types for Polymorphic Variants /we defined type inference for polymorphic variants with recursive set-theoretic types (type are defined coinductively? with a couple of standard restrictions). https://urldefense.com/v3/__https://www.irif.fr/*gc/papers/icfp16.pdf__;fg!!IBzWLUs!QYIv5kZfRZ_sM_dbcvKdrXLsHb-tjd_4jpTeLE-n3m-E8TJ2qqx4c-2QqB1nepcRXZPlaUrqjL2yHCM5-OiV$ More generally, you may want to refer to Tommaso Petrucciani's PhD thesis /Polymorphic set-theoretic types for functional languages/ which studies type inference for recursive set-theoretic types (they can encode ADT' s via products and unions), which uses and improves some results of Stephen Dolan' s PhD thesis as well as of the paper cited above. https://urldefense.com/v3/__http://www.theses.fr/2019USPCC067__;!!IBzWLUs!QYIv5kZfRZ_sM_dbcvKdrXLsHb-tjd_4jpTeLE-n3m-E8TJ2qqx4c-2QqB1nepcRXZPlaUrqjL2yHFyPLk_c$ Hope it is useful Cheers Beppe On 17/06/2022 09.40, Aaron Gray wrote: > [ The Types Forum,http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > I am interested if there is any work on the subtyping of mutually > recursive algebraic data types. I am wanting an algorithm for purposes > of implementing an object oriented programming language with ADT's > which lower onto a virtual class implementation which can support > mutually recursive behavior, but need the typ checking and inference > at the ADT level. > > Theres a number of papers and projects in this area I have came across > but none of them actually tackle algebraic data types properly let > alone mutually recursive ones. > > A number inspired by Stephen Dolan's PhD Thesis and MLsub, his implementation. > > - Practical Subtyping for Curry-Style Languages by Rodolphe Lepigre > and Christophe Raffalli - subml -https://urldefense.com/v3/__https://github.com/rlepigre/subml__;!!IBzWLUs!ROzY30gWHR0LPvTTZLo_Ep7ErCu0LhX2jrPKbFJ9uhVgSSx659leOfq_pNrPSAGgLExea89yhX9iVce14nA987dFVoNzXhSpE6cZJg$ > - The Simple Essence of Algebraic Subtyping, Lionel Parreaux and > simple-sub implementation -https://urldefense.com/v3/__https://github.com/LPTK/simple-sub__;!!IBzWLUs!ROzY30gWHR0LPvTTZLo_Ep7ErCu0LhX2jrPKbFJ9uhVgSSx659leOfq_pNrPSAGgLExea89yhX9iVce14nA987dFVoNzXhS4dNcEiw$ > - A Mechanical Soundness Proof for Subtyping Over Recursive Types > Timothy Jones David J. Pearce - > https://urldefense.com/v3/__https://github.com/zmthy/recursive-types__;!!IBzWLUs!ROzY30gWHR0LPvTTZLo_Ep7ErCu0LhX2jrPKbFJ9uhVgSSx659leOfq_pNrPSAGgLExea89yhX9iVce14nA987dFVoNzXhRACugkxw$ > > None of these seem to deal with mutually recursive data types. > > I am interested in the papproach of using codata/coinduction and > coalgebras and possibly bisimulation in order to deal with the > mutually recursive nature of real world mutually recursive algebraic > data types like for instance AST's of real world complex computer > languages. > > Any projects, papers, thoughts, or implementations would be of interest. > > Regards, > > Aaron From roberto at dicosmo.org Sun Jun 19 10:47:38 2022 From: roberto at dicosmo.org (Roberto Di Cosmo) Date: Sun, 19 Jun 2022 16:47:38 +0200 Subject: [TYPES] subtyping of mutually recursive algebraic data types In-Reply-To: References: Message-ID: Dear Aaron, probably not exactly what you are looking for, but this old article that addresses subtyping of recursive types may contain some useful piece of information. Roberto Di Cosmo, Fran?ois Pottier, and Didier R?my. Subtyping recursive types modulo associative commutative products. Typed Lambda Calculus and Applications, 2005, https://urldefense.com/v3/__http://dx.doi.org/10.1007/11417170_14__;!!IBzWLUs!W56eVak-fIjNK6SjoBie6PabAIqpQ2eJspOLTnNw5nIhHa4vYvun3qyAgz-hLNyiR4KFU7v7RxzWu8WcPm3w43kqOf_G$ You can get a green open access copy here: https://urldefense.com/v3/__https://hal.archives-ouvertes.fr/hal-00149563__;!!IBzWLUs!W56eVak-fIjNK6SjoBie6PabAIqpQ2eJspOLTnNw5nIhHa4vYvun3qyAgz-hLNyiR4KFU7v7RxzWu8WcPm3w49yEkAm1$ Cheers -- Roberto On Fri, 17 Jun 2022 at 09:40, Aaron Gray wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > I am interested if there is any work on the subtyping of mutually > recursive algebraic data types. I am wanting an algorithm for purposes > of implementing an object oriented programming language with ADT's > which lower onto a virtual class implementation which can support > mutually recursive behavior, but need the typ checking and inference > at the ADT level. > > Theres a number of papers and projects in this area I have came across > but none of them actually tackle algebraic data types properly let > alone mutually recursive ones. > > A number inspired by Stephen Dolan's PhD Thesis and MLsub, his > implementation. > > - Practical Subtyping for Curry-Style Languages by Rodolphe Lepigre > and Christophe Raffalli - subml - > https://urldefense.com/v3/__https://github.com/rlepigre/subml__;!!IBzWLUs!ROzY30gWHR0LPvTTZLo_Ep7ErCu0LhX2jrPKbFJ9uhVgSSx659leOfq_pNrPSAGgLExea89yhX9iVce14nA987dFVoNzXhSpE6cZJg$ > - The Simple Essence of Algebraic Subtyping, Lionel Parreaux and > simple-sub implementation - > https://urldefense.com/v3/__https://github.com/LPTK/simple-sub__;!!IBzWLUs!ROzY30gWHR0LPvTTZLo_Ep7ErCu0LhX2jrPKbFJ9uhVgSSx659leOfq_pNrPSAGgLExea89yhX9iVce14nA987dFVoNzXhS4dNcEiw$ > - A Mechanical Soundness Proof for Subtyping Over Recursive Types > Timothy Jones David J. Pearce - > > https://urldefense.com/v3/__https://github.com/zmthy/recursive-types__;!!IBzWLUs!ROzY30gWHR0LPvTTZLo_Ep7ErCu0LhX2jrPKbFJ9uhVgSSx659leOfq_pNrPSAGgLExea89yhX9iVce14nA987dFVoNzXhRACugkxw$ > > None of these seem to deal with mutually recursive data types. > > I am interested in the papproach of using codata/coinduction and > coalgebras and possibly bisimulation in order to deal with the > mutually recursive nature of real world mutually recursive algebraic > data types like for instance AST's of real world complex computer > languages. > > Any projects, papers, thoughts, or implementations would be of interest. > > Regards, > > Aaron > From aaronngray.lists at gmail.com Thu Jun 23 11:29:09 2022 From: aaronngray.lists at gmail.com (Aaron Gray) Date: Thu, 23 Jun 2022 16:29:09 +0100 Subject: [TYPES] subtyping of mutually recursive algebraic data types In-Reply-To: References: Message-ID: On Fri, 17 Jun 2022 at 18:00, Mark Sheldon wrote: > > We deal with this topic in our book, Design Concepts in Programming Languages (https://urldefense.com/v3/__https://mitpress.mit.edu/books/design-concepts-programming-languages__;!!IBzWLUs!VMszV1CswUJMokl4bq4nZ2MiwksJZ8Yv9-8MP3BH1wxJXGi_EuLL1aoglnuW3Ox9O6RYStjSg30TbV4z0GKs7OlslS5BDu4RWPR2mA$ ). See Chapter 12. There is a section on ?Subtyping of Recursive Types on pages 706?707, Mark, thank you I have ordered a copy of your book, I have a copy of TAPL but Chapter 12 seems pretty limited. Thanks for the other two papers, Aaron > > Here are relevant references given in the Notes section of Chapter 12 on page 767: > > Kozen, Palsberg, Schwartzbach. Efficent recursive subtyping. POPL 93. > Gapayev, Levin, Pierce. Recursive subtyping revealed. ICFP 00. > Pierce. Types and Programming Languages. MIT Press. 2002. Chapter 12. > > > I hope this is useful! > > -Mark > > Mark A. Sheldon > Associate Teaching Professor > Department of Computer Science > Tufts University > > On 17Jun, 2022, at 03:40, Aaron Gray wrote: > > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > I am interested if there is any work on the subtyping of mutually > recursive algebraic data types. I am wanting an algorithm for purposes > of implementing an object oriented programming language with ADT's > which lower onto a virtual class implementation which can support > mutually recursive behavior, but need the typ checking and inference > at the ADT level. > > Theres a number of papers and projects in this area I have came across > but none of them actually tackle algebraic data types properly let > alone mutually recursive ones. > > A number inspired by Stephen Dolan's PhD Thesis and MLsub, his implementation. > > - Practical Subtyping for Curry-Style Languages by Rodolphe Lepigre > and Christophe Raffalli - subml - https://urldefense.com/v3/__https://github.com/rlepigre/subml__;!!IBzWLUs!ROzY30gWHR0LPvTTZLo_Ep7ErCu0LhX2jrPKbFJ9uhVgSSx659leOfq_pNrPSAGgLExea89yhX9iVce14nA987dFVoNzXhSpE6cZJg$ > - The Simple Essence of Algebraic Subtyping, Lionel Parreaux and > simple-sub implementation - https://urldefense.com/v3/__https://github.com/LPTK/simple-sub__;!!IBzWLUs!ROzY30gWHR0LPvTTZLo_Ep7ErCu0LhX2jrPKbFJ9uhVgSSx659leOfq_pNrPSAGgLExea89yhX9iVce14nA987dFVoNzXhS4dNcEiw$ > - A Mechanical Soundness Proof for Subtyping Over Recursive Types > Timothy Jones David J. Pearce - > https://urldefense.com/v3/__https://github.com/zmthy/recursive-types__;!!IBzWLUs!ROzY30gWHR0LPvTTZLo_Ep7ErCu0LhX2jrPKbFJ9uhVgSSx659leOfq_pNrPSAGgLExea89yhX9iVce14nA987dFVoNzXhRACugkxw$ > > None of these seem to deal with mutually recursive data types. > > I am interested in the papproach of using codata/coinduction and > coalgebras and possibly bisimulation in order to deal with the > mutually recursive nature of real world mutually recursive algebraic > data types like for instance AST's of real world complex computer > languages. > > Any projects, papers, thoughts, or implementations would be of interest. > > Regards, > > Aaron > > -- Aaron Gray Independent Open Source Software Engineer, Computer Language Researcher, Information Theorist, and amateur computer scientist. From sheldon at alum.mit.edu Thu Jun 23 15:19:59 2022 From: sheldon at alum.mit.edu (Mark Sheldon) Date: Thu, 23 Jun 2022 15:19:59 -0400 Subject: [TYPES] subtyping of mutually recursive algebraic data types In-Reply-To: References: Message-ID: Hi, Aaron, I?m honored! :-) I didn?t mean to make a sales pitch ? I figured if you had access to a copy it might help, and if not, the references would do it. Others have provided some more recent references, too, and I hope you?re making progress. Thanks, and I hope you find our book a useful addition to your collection! -Mark > On 23Jun, 2022, at 11:29, Aaron Gray wrote: > > On Fri, 17 Jun 2022 at 18:00, Mark Sheldon wrote: >> >> We deal with this topic in our book, Design Concepts in Programming Languages (https://urldefense.com/v3/__https://mitpress.mit.edu/books/design-concepts-programming-languages__;!!IBzWLUs!TJHPwJx6mfjdKduqLQoPQCY45K3obf1hr7CB-4Xw0Iy0-6oRFCtaHvPsq7SP6VflJQzBGmSZBbPNycoz7HQBbGPjpO18glvJ$ ). See Chapter 12. There is a section on ?Subtyping of Recursive Types on pages 706?707, > > Mark, thank you I have ordered a copy of your book, I have a copy of > TAPL but Chapter 12 seems pretty limited. > > Thanks for the other two papers, > > Aaron > >> >> Here are relevant references given in the Notes section of Chapter 12 on page 767: >> >> Kozen, Palsberg, Schwartzbach. Efficent recursive subtyping. POPL 93. >> Gapayev, Levin, Pierce. Recursive subtyping revealed. ICFP 00. >> Pierce. Types and Programming Languages. MIT Press. 2002. Chapter 12. >> >> >> I hope this is useful! >> >> -Mark >> >> Mark A. Sheldon >> Associate Teaching Professor >> Department of Computer Science >> Tufts University >> >> On 17Jun, 2022, at 03:40, Aaron Gray wrote: >> >> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] >> >> I am interested if there is any work on the subtyping of mutually >> recursive algebraic data types. I am wanting an algorithm for purposes >> of implementing an object oriented programming language with ADT's >> which lower onto a virtual class implementation which can support >> mutually recursive behavior, but need the typ checking and inference >> at the ADT level. >> >> Theres a number of papers and projects in this area I have came across >> but none of them actually tackle algebraic data types properly let >> alone mutually recursive ones. >> >> A number inspired by Stephen Dolan's PhD Thesis and MLsub, his implementation. >> >> - Practical Subtyping for Curry-Style Languages by Rodolphe Lepigre >> and Christophe Raffalli - subml - https://urldefense.com/v3/__https://github.com/rlepigre/subml__;!!IBzWLUs!ROzY30gWHR0LPvTTZLo_Ep7ErCu0LhX2jrPKbFJ9uhVgSSx659leOfq_pNrPSAGgLExea89yhX9iVce14nA987dFVoNzXhSpE6cZJg$ >> - The Simple Essence of Algebraic Subtyping, Lionel Parreaux and >> simple-sub implementation - https://urldefense.com/v3/__https://github.com/LPTK/simple-sub__;!!IBzWLUs!ROzY30gWHR0LPvTTZLo_Ep7ErCu0LhX2jrPKbFJ9uhVgSSx659leOfq_pNrPSAGgLExea89yhX9iVce14nA987dFVoNzXhS4dNcEiw$ >> - A Mechanical Soundness Proof for Subtyping Over Recursive Types >> Timothy Jones David J. Pearce - >> https://urldefense.com/v3/__https://github.com/zmthy/recursive-types__;!!IBzWLUs!ROzY30gWHR0LPvTTZLo_Ep7ErCu0LhX2jrPKbFJ9uhVgSSx659leOfq_pNrPSAGgLExea89yhX9iVce14nA987dFVoNzXhRACugkxw$ >> >> None of these seem to deal with mutually recursive data types. >> >> I am interested in the papproach of using codata/coinduction and >> coalgebras and possibly bisimulation in order to deal with the >> mutually recursive nature of real world mutually recursive algebraic >> data types like for instance AST's of real world complex computer >> languages. >> >> Any projects, papers, thoughts, or implementations would be of interest. >> >> Regards, >> >> Aaron >> >> > > > -- > Aaron Gray > > Independent Open Source Software Engineer, Computer Language > Researcher, Information Theorist, and amateur computer scientist. From aaronngray.lists at gmail.com Thu Jun 23 15:27:09 2022 From: aaronngray.lists at gmail.com (Aaron Gray) Date: Thu, 23 Jun 2022 20:27:09 +0100 Subject: [TYPES] subtyping of mutually recursive algebraic data types In-Reply-To: References: Message-ID: On Thu, 23 Jun 2022 at 20:20, Mark Sheldon wrote: > > Hi, Aaron, > > I?m honored! :-) I didn?t mean to make a sales pitch ? I figured if you had access to a copy it might help, and if not, the references would do it. Others have provided some more recent references, too, and I hope you?re making progress. Mark, Thank you, this is a very long term project for me, and subtyping has become a monster thats been tamed on many levels but still keeps escaping, you could write a book on it alone, I am surprised no one has done that yet :) Regards, Aaron > > Thanks, and I hope you find our book a useful addition to your collection! > > -Mark > > > On 23Jun, 2022, at 11:29, Aaron Gray wrote: > > > > On Fri, 17 Jun 2022 at 18:00, Mark Sheldon wrote: > >> > >> We deal with this topic in our book, Design Concepts in Programming Languages (https://urldefense.com/v3/__https://mitpress.mit.edu/books/design-concepts-programming-languages__;!!IBzWLUs!QAv4EtwSw_gYVTzSrqYnAM1svOt58VpLCGnhStxGVIVJTVRGfj8Wwij4pYR3JT6Rkvb5maOVIic3qaDBjZgAitRRa3g2KapfhG-5NA$ ). See Chapter 12. There is a section on ?Subtyping of Recursive Types on pages 706?707, > > > > Mark, thank you I have ordered a copy of your book, I have a copy of > > TAPL but Chapter 12 seems pretty limited. > > > > Thanks for the other two papers, > > > > Aaron > > > >> > >> Here are relevant references given in the Notes section of Chapter 12 on page 767: > >> > >> Kozen, Palsberg, Schwartzbach. Efficent recursive subtyping. POPL 93. > >> Gapayev, Levin, Pierce. Recursive subtyping revealed. ICFP 00. > >> Pierce. Types and Programming Languages. MIT Press. 2002. Chapter 12. > >> > >> > >> I hope this is useful! > >> > >> -Mark > >> > >> Mark A. Sheldon > >> Associate Teaching Professor > >> Department of Computer Science > >> Tufts University > >> > >> On 17Jun, 2022, at 03:40, Aaron Gray wrote: > >> > >> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > >> > >> I am interested if there is any work on the subtyping of mutually > >> recursive algebraic data types. I am wanting an algorithm for purposes > >> of implementing an object oriented programming language with ADT's > >> which lower onto a virtual class implementation which can support > >> mutually recursive behavior, but need the typ checking and inference > >> at the ADT level. > >> > >> Theres a number of papers and projects in this area I have came across > >> but none of them actually tackle algebraic data types properly let > >> alone mutually recursive ones. > >> > >> A number inspired by Stephen Dolan's PhD Thesis and MLsub, his implementation. > >> > >> - Practical Subtyping for Curry-Style Languages by Rodolphe Lepigre > >> and Christophe Raffalli - subml - https://urldefense.com/v3/__https://github.com/rlepigre/subml__;!!IBzWLUs!ROzY30gWHR0LPvTTZLo_Ep7ErCu0LhX2jrPKbFJ9uhVgSSx659leOfq_pNrPSAGgLExea89yhX9iVce14nA987dFVoNzXhSpE6cZJg$ > >> - The Simple Essence of Algebraic Subtyping, Lionel Parreaux and > >> simple-sub implementation - https://urldefense.com/v3/__https://github.com/LPTK/simple-sub__;!!IBzWLUs!ROzY30gWHR0LPvTTZLo_Ep7ErCu0LhX2jrPKbFJ9uhVgSSx659leOfq_pNrPSAGgLExea89yhX9iVce14nA987dFVoNzXhS4dNcEiw$ > >> - A Mechanical Soundness Proof for Subtyping Over Recursive Types > >> Timothy Jones David J. Pearce - > >> https://urldefense.com/v3/__https://github.com/zmthy/recursive-types__;!!IBzWLUs!ROzY30gWHR0LPvTTZLo_Ep7ErCu0LhX2jrPKbFJ9uhVgSSx659leOfq_pNrPSAGgLExea89yhX9iVce14nA987dFVoNzXhRACugkxw$ > >> > >> None of these seem to deal with mutually recursive data types. > >> > >> I am interested in the papproach of using codata/coinduction and > >> coalgebras and possibly bisimulation in order to deal with the > >> mutually recursive nature of real world mutually recursive algebraic > >> data types like for instance AST's of real world complex computer > >> languages. > >> > >> Any projects, papers, thoughts, or implementations would be of interest. > >> > >> Regards, > >> > >> Aaron > >> > >> > > > > > > -- > > Aaron Gray > > > > Independent Open Source Software Engineer, Computer Language > > Researcher, Information Theorist, and amateur computer scientist. > -- Aaron Gray Independent Open Source Software Engineer, Computer Language Researcher, Information Theorist, and amateur computer scientist. From neelakantan.krishnaswami at gmail.com Fri Jun 24 09:26:18 2022 From: neelakantan.krishnaswami at gmail.com (Neel Krishnaswami) Date: Fri, 24 Jun 2022 14:26:18 +0100 Subject: [TYPES] Semantics of modes in logic programming? In-Reply-To: References: <76cc3048bcff055661c084cc3ff9dde3436dd674.camel@imperial.ac.uk> <20220609151021.GA10454@topoi.pooq.com> Message-ID: Hello, I'm interested in the semantics of mode systems in logic programming, especially (a) mode systems more sophisticated than simple input or output modes, and (b) denotational semantics of logic programs with modes. Uday Reddy's 1992 paper "A typed foundation for directional logic programming" (https://urldefense.com/v3/__https://www.cs.bham.ac.uk/*udr/papers/directional.pdf__;fg!!IBzWLUs!RIsOJV9x2aZaYUcdxebrICDz_vREN4r14OX46bY1vpRhC6gHz6PZnsDR9JcDg9vQSGbGNvsoOfl3Kks_ocdKMUcJyqKwVlveYJZj8Q$ ) gives a beautiful mode system based on classical linear logic, and he shows it has a lot of really great operational properties. I'd be especially interested in a denotational (especially categorical) semantics for this language, but want to cast the net broadly in this question. Thanks! Best, Neel From aaronngray.lists at gmail.com Thu Jul 14 15:02:05 2022 From: aaronngray.lists at gmail.com (Aaron Gray) Date: Thu, 14 Jul 2022 20:02:05 +0100 Subject: [TYPES] subtyping of mutually recursive algebraic data types In-Reply-To: References: Message-ID: Matthew, Thank you for showing me Motoko's implementation, sorry its taken me so long to get back to you but theres been a wealth of replies, and still a lot to look at properly. Motoko looks like very neat and reasonably small SML code, so I will take a proper look at it Its interesting to me as it implements lattice like/based LUB and GLB code, which is how I am intending on implementing the core of the type system as well, and with kinds and interval types. I was originally looking for the use of coinduction for solving subtyping for mutually recursive datatypes which Frank's paper and implementation gives, so am looking at that currently still. Regards, Aaron On Sun, 19 Jun 2022 at 00:15, Matthew A. Hammer wrote: > > PS: There's also a playground online to support experiments in the > browser, and no downloading: > https://urldefense.com/v3/__https://m7sm4-2iaaa-aaaab-qabra-cai.raw.ic0.app/__;!!IBzWLUs!WgY_4vSpPi0jgq_qGkVH35MzzXX63D112L28FuPqcfEjHvkU_CsX-zWRluiPZcYefOgW5zCifZIHBzeFnriASFsur_vJxTpUlGb3Tg$ > > And I realize that URL is starting out looking quite strange, even > before mailing list mangling. The playground is partially written in > Motoko itself, and is running on "Web3", so that's why. You can see > the source on good old Web2, here: > https://urldefense.com/v3/__https://github.com/dfinity/motoko-playground__;!!IBzWLUs!WgY_4vSpPi0jgq_qGkVH35MzzXX63D112L28FuPqcfEjHvkU_CsX-zWRluiPZcYefOgW5zCifZIHBzeFnriASFsur_vJxTo18VoVVg$ > > Happy to talk further, if it seems interesting or you have questions. > > Kind wishes, > Matthew > > On Sat, Jun 18, 2022 at 5:08 PM Matthew A. Hammer > wrote: > > > > Hi Aaron, > > > > Due to oddities of the mailing list, I didn't get the original message > > you sent, but from the title and other responses that quote you, I see > > that you are currently involved in designing a new OO language with > > FP-style data types, and subtyping. > > > > Have you given Motoko a look? > > > > In either case, I wonder how it compares to the vision you have. > > > > If you are curious about the type system and subtyping checks, I'd > > start here: (hopefully these URLs stay usable; I worry.) > > https://urldefense.com/v3/__https://github.com/dfinity/motoko/blob/master/src/mo_types/type.mli__;!!IBzWLUs!WgY_4vSpPi0jgq_qGkVH35MzzXX63D112L28FuPqcfEjHvkU_CsX-zWRluiPZcYefOgW5zCifZIHBzeFnriASFsur_vJxTpSGErMkA$ > > > > And here: > > https://urldefense.com/v3/__https://github.com/dfinity/motoko/blob/master/src/mo_types/type.ml__;!!IBzWLUs!WgY_4vSpPi0jgq_qGkVH35MzzXX63D112L28FuPqcfEjHvkU_CsX-zWRluiPZcYefOgW5zCifZIHBzeFnriASFsur_vJxTpYJ_e7DQ$ > > > > The general sales pitch and some small examples are here: > > https://urldefense.com/v3/__https://internetcomputer.org/docs/current/developer-docs/build/languages/motoko/__;!!IBzWLUs!WgY_4vSpPi0jgq_qGkVH35MzzXX63D112L28FuPqcfEjHvkU_CsX-zWRluiPZcYefOgW5zCifZIHBzeFnriASFsur_vJxTpFfIFV4w$ > > > > The compiler repo has lots of tests with more examples that > > demonstrate how the language and typing work. See the .mo files under > > tests. > > > > My team implemented the subtyping check, which I understand from > > talking with them that it is tricky. I'm not familiar with the > > internals myself, but you could reach out to Andreas Rossberg, Claudio > > Russo and Joachim Breitner who did that work (and most other parts of > > the language design and implementation). > > > > KInd wishes, > > Matthew > > > > On Sat, Jun 18, 2022 at 8:09 AM Frank Pfenning wrote: > > > > > > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > > > > > You might find our recent ESOP paper relevant: > > > > > > Zeeshan Lakhani, Ankush Das, Henry DeYoung, Andreia Mordido, Frank Pfenning: > > > Polarized Subtyping. ESOP 2022: 431-461 > > > https://urldefense.com/v3/__https://link.springer.com/chapter/10.1007/978-3-030-99336-8_16__;!!IBzWLUs!QrMnoLw8qFRxtzf2zu5w8Gc14aO6rhn_cCBMv4Q0dczTVPBFrRikSVu7fiARjhLIovnBm3oBBgYJ2dYwzqkdvV8$ > > > > > > There are some further references in that paper in the related work section. > > > A version with polymorphism, but without explicit polarization > > > (essentially: all types > > > are interpreted coinductively because they are session types) can be found > > > in > > > > > > Ankush Das, Henry DeYoung, Andreia Mordido, Frank Pfenning: > > > Subtyping on Nested Polymorphic Session Types. CoRR abs/2103.15193 (2021) > > > https://urldefense.com/v3/__https://arxiv.org/abs/2103.15193__;!!IBzWLUs!QrMnoLw8qFRxtzf2zu5w8Gc14aO6rhn_cCBMv4Q0dczTVPBFrRikSVu7fiARjhLIovnBm3oBBgYJ2dYwMw8Y7mY$ > > > > > > There we show that a natural formulation of the problem in the presence of > > > polymorphism > > > is undecidable, but also give an algorithm that has performed well for us > > > in practice. > > > > > > - Frank > > > > > > On Fri, Jun 17, 2022 at 9:11 AM Aaron Gray > > > wrote: > > > > > > > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > > > > ] > > > > > > > > I am interested if there is any work on the subtyping of mutually > > > > recursive algebraic data types. I am wanting an algorithm for purposes > > > > of implementing an object oriented programming language with ADT's > > > > which lower onto a virtual class implementation which can support > > > > mutually recursive behavior, but need the typ checking and inference > > > > at the ADT level. > > > > > > > > Theres a number of papers and projects in this area I have came across > > > > but none of them actually tackle algebraic data types properly let > > > > alone mutually recursive ones. > > > > > > > > A number inspired by Stephen Dolan's PhD Thesis and MLsub, his > > > > implementation. > > > > > > > > - Practical Subtyping for Curry-Style Languages by Rodolphe Lepigre > > > > and Christophe Raffalli - subml - > > > > https://urldefense.com/v3/__https://github.com/rlepigre/subml__;!!IBzWLUs!ROzY30gWHR0LPvTTZLo_Ep7ErCu0LhX2jrPKbFJ9uhVgSSx659leOfq_pNrPSAGgLExea89yhX9iVce14nA987dFVoNzXhSpE6cZJg$ > > > > - The Simple Essence of Algebraic Subtyping, Lionel Parreaux and > > > > simple-sub implementation - > > > > https://urldefense.com/v3/__https://github.com/LPTK/simple-sub__;!!IBzWLUs!ROzY30gWHR0LPvTTZLo_Ep7ErCu0LhX2jrPKbFJ9uhVgSSx659leOfq_pNrPSAGgLExea89yhX9iVce14nA987dFVoNzXhS4dNcEiw$ > > > > - A Mechanical Soundness Proof for Subtyping Over Recursive Types > > > > Timothy Jones David J. Pearce - > > > > > > > > https://urldefense.com/v3/__https://github.com/zmthy/recursive-types__;!!IBzWLUs!ROzY30gWHR0LPvTTZLo_Ep7ErCu0LhX2jrPKbFJ9uhVgSSx659leOfq_pNrPSAGgLExea89yhX9iVce14nA987dFVoNzXhRACugkxw$ > > > > > > > > None of these seem to deal with mutually recursive data types. > > > > > > > > I am interested in the papproach of using codata/coinduction and > > > > coalgebras and possibly bisimulation in order to deal with the > > > > mutually recursive nature of real world mutually recursive algebraic > > > > data types like for instance AST's of real world complex computer > > > > languages. > > > > > > > > Any projects, papers, thoughts, or implementations would be of interest. > > > > > > > > Regards, > > > > > > > > Aaron > > > > > > > > > > > > > -- > > > Frank Pfenning, Professor > > > Computer Science Department > > > Carnegie Mellon University > > > Pittsburgh, PA 15213-3891 > > > > > > https://urldefense.com/v3/__http://www.cs.cmu.edu/*fp__;fg!!IBzWLUs!QrMnoLw8qFRxtzf2zu5w8Gc14aO6rhn_cCBMv4Q0dczTVPBFrRikSVu7fiARjhLIovnBm3oBBgYJ2dYwrgSsDME$ > > > +1 412 268-6343 > > > GHC 6017 -- Aaron Gray Independent Open Source Software Engineer, Computer Language Researcher, Information Theorist, and amateur computer scientist. From fdhzs2010 at hotmail.com Sun Aug 14 11:25:26 2022 From: fdhzs2010 at hotmail.com (Jason Hu) Date: Sun, 14 Aug 2022 15:25:26 +0000 Subject: [TYPES] reference request: MLTT with Russell's non-cumulative universes Message-ID: Hi all, I am writing to see if anyone has formalized a formulation MLTT with non-cumulative universes. This type theory is useful and interesting and is a foundation for, e.g. Agda. In particular, I would like to see some proofs of some properties like type uniqueness. I saw in many places that people say with non-cumulative universes, every term has a unique type (up to equivalence). However, it does not seem very obvious how to prove it easily by syntactic method. For example, consider function application t s : T1 [ s ] and t s : T2 [ s ] where [ s ] denotes substitution of the topmost variable only. Now we want to prove T1 [ s ] and T2 [ s ] are equivalent. However, induction on t only shows that for some S1 and S2, such that t : (x : S1). T1 and t : (x : S2). T2 ==> : (x : S1). T1 ~ (x : S2). T2 where ~ is the definitional equivalence relation, but then we are stuck, because we are not able to show T1 ~ T2 without doing a logical relation argument. The type uniqueness property is important to prove the property that every type lives in precisely one universe, where we need another property that also needs logical relations to establish: Set i ~ Set j ==> i = j Is there any document that systematically looks into non-cumulativity? Many I read only talk about cumulative universes and non-cumulativity seems often elided. Thanks, Jason From aaronngray.lists at gmail.com Tue Aug 9 08:52:03 2022 From: aaronngray.lists at gmail.com (Aaron Gray) Date: Tue, 9 Aug 2022 13:52:03 +0100 Subject: [TYPES] subtyping of mutually recursive algebraic data types In-Reply-To: <380ead85-e0a1-2d16-0226-79ddfeae5e81@irif.fr> References: <380ead85-e0a1-2d16-0226-79ddfeae5e81@irif.fr> Message-ID: Hi Giuseppi, Sorry it has taken so long to get back to you theres been such a rich wealth of replies and papers. I am starting to read your two papers on Semantic Subtyping as they seem a good place to start before Set-Theoretic Types for Polymorphic Variants and Tommaso Petrucciani's PhD thesis. I have a pile of papers on sub typing I have read over the years but this and the coinduction approach are relatively new to me. CDuce looks very interesting so I will study that in conjunction with your papers. Many thanks Aaron On Sat, 18 Jun 2022 at 23:07, Giuseppe Castagna wrote: > > In our ICFP 16 Paper Set-Theoretic Types for Polymorphic Variants we defined type inference for polymorphic variants with recursive set-theoretic types (type are defined coinductively with a couple of standard restrictions). https://urldefense.com/v3/__https://www.irif.fr/*gc/papers/icfp16.pdf__;fg!!IBzWLUs!XKdWD60h2cKWz0GzrVroGQkYYWMHIJXtEbZmQoUmf_BRSU-sEdQ6qtV93GrJXQ0es1B5E_jW5c_2BELiElxdKqHpQnSA9LIEDfuiNg$ > > More generally, you may want to refer to Tommaso Petrucciani's PhD thesis Polymorphic set-theoretic types for functional languages which studies type inference for recursive set-theoretic types (they can encode ADT' s via products and unions), which uses and improves some results of Stephen Dolan' s PhD thesis as well as of the paper cited above. https://urldefense.com/v3/__http://www.theses.fr/2019USPCC067__;!!IBzWLUs!XKdWD60h2cKWz0GzrVroGQkYYWMHIJXtEbZmQoUmf_BRSU-sEdQ6qtV93GrJXQ0es1B5E_jW5c_2BELiElxdKqHpQnSA9LKwx3nBHQ$ > > Hope it is useful > > Cheers > > Beppe > > > On 17/06/2022 09.40, Aaron Gray wrote: > > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > I am interested if there is any work on the subtyping of mutually > recursive algebraic data types. I am wanting an algorithm for purposes > of implementing an object oriented programming language with ADT's > which lower onto a virtual class implementation which can support > mutually recursive behavior, but need the typ checking and inference > at the ADT level. > > Theres a number of papers and projects in this area I have came across > but none of them actually tackle algebraic data types properly let > alone mutually recursive ones. > > A number inspired by Stephen Dolan's PhD Thesis and MLsub, his implementation. > > - Practical Subtyping for Curry-Style Languages by Rodolphe Lepigre > and Christophe Raffalli - subml - https://urldefense.com/v3/__https://github.com/rlepigre/subml__;!!IBzWLUs!ROzY30gWHR0LPvTTZLo_Ep7ErCu0LhX2jrPKbFJ9uhVgSSx659leOfq_pNrPSAGgLExea89yhX9iVce14nA987dFVoNzXhSpE6cZJg$ > - The Simple Essence of Algebraic Subtyping, Lionel Parreaux and > simple-sub implementation - https://urldefense.com/v3/__https://github.com/LPTK/simple-sub__;!!IBzWLUs!ROzY30gWHR0LPvTTZLo_Ep7ErCu0LhX2jrPKbFJ9uhVgSSx659leOfq_pNrPSAGgLExea89yhX9iVce14nA987dFVoNzXhS4dNcEiw$ > - A Mechanical Soundness Proof for Subtyping Over Recursive Types > Timothy Jones David J. Pearce - > https://urldefense.com/v3/__https://github.com/zmthy/recursive-types__;!!IBzWLUs!ROzY30gWHR0LPvTTZLo_Ep7ErCu0LhX2jrPKbFJ9uhVgSSx659leOfq_pNrPSAGgLExea89yhX9iVce14nA987dFVoNzXhRACugkxw$ > > None of these seem to deal with mutually recursive data types. > > I am interested in the papproach of using codata/coinduction and > coalgebras and possibly bisimulation in order to deal with the > mutually recursive nature of real world mutually recursive algebraic > data types like for instance AST's of real world complex computer > languages. > > Any projects, papers, thoughts, or implementations would be of interest. > > Regards, > > Aaron From sandro.stucki at gmail.com Mon Aug 15 17:28:41 2022 From: sandro.stucki at gmail.com (Sandro Stucki) Date: Mon, 15 Aug 2022 23:28:41 +0200 Subject: [TYPES] reference request: MLTT with Russell's non-cumulative universes In-Reply-To: References: Message-ID: Hi Jason! If I understand correctly, you're looking for a syntactic proof of uniqueness of types, and the crucial property you need to make progress here is injectivity of the Pi type constructor (Pi-injectivity). As usual, the devil is in the details, but if you're happy with a formulation of type theory that 1) only has Pi types and universes, but no Sigma types (aka a pure type system) and 2) treats types and terms up to (untyped) beta-equivalence (no eta-conversions) then Pi-injectivity is relatively easy to prove syntactically (via Church-Rosser). I believe that pure type systems (PTS) are sufficient for expressing the sort of non-cumulative universes you want, and that uniqueness of types holds for the relevant class of PTSs. A nice reference for PTSs is Barendregt's "Lambda calculi with types" (1993) -- the chapter, not the book. See Lemma 5.2.21 (p. 109) for a proof of uniqueness of types (I believe the system you have in mind should indeed be singly-sorted). Since you mentioned Agda: I mechanized the basic meta-theory of PTSs (including Pi-injectivity, but not uniqueness of types) a while ago in Agda. It probably won't type-check using an up-to-date version of Agda, but it might still be useful to get the basic ideas: https://urldefense.com/v3/__https://github.com/sstucki/pts-agda__;!!IBzWLUs!QXpaFzibWjXFsmwg69eOfmT90TG_uHJIUXlKmGHrJGyoFxGZPBERPgCMbUpJ1Uvo-3K1SJ31ejysKwPoWcsknRHg1ObxFKH-Jh8$ Cheers /Sandro On Mon, Aug 15, 2022 at 10:14 PM Jason Hu wrote: > > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Hi all, > > I am writing to see if anyone has formalized a formulation MLTT with non-cumulative universes. This type theory is useful and interesting and is a foundation for, e.g. Agda. In particular, I would like to see some proofs of some properties like type uniqueness. I saw in many places that people say with non-cumulative universes, every term has a unique type (up to equivalence). However, it does not seem very obvious how to prove it easily by syntactic method. For example, consider function application > > t s : T1 [ s ] and t s : T2 [ s ] > > where [ s ] denotes substitution of the topmost variable only. Now we want to prove T1 [ s ] and T2 [ s ] are equivalent. However, induction on t only shows that for some S1 and S2, such that > > t : (x : S1). T1 and t : (x : S2). T2 ==> : (x : S1). T1 ~ (x : S2). T2 > > where ~ is the definitional equivalence relation, but then we are stuck, because we are not able to show T1 ~ T2 without doing a logical relation argument. > > The type uniqueness property is important to prove the property that every type lives in precisely one universe, where we need another property that also needs logical relations to establish: > > Set i ~ Set j ==> i = j > > Is there any document that systematically looks into non-cumulativity? Many I read only talk about cumulative universes and non-cumulativity seems often elided. > > Thanks, > Jason > From fdhzs2010 at hotmail.com Mon Aug 15 21:12:49 2022 From: fdhzs2010 at hotmail.com (Jason Hu) Date: Tue, 16 Aug 2022 01:12:49 +0000 Subject: [TYPES] reference request: MLTT with Russell's non-cumulative universes In-Reply-To: References: Message-ID: Hi Sandro, Thanks for your reference. I don?t actually necessarily mean a syntactic proof but is more generally wondering whether these properties have been looked into in details and if so, what is the earliest work. I will definitely look into your PTS mechanization. Thanks, Jason From: Sandro Stucki Sent: Monday, August 15, 2022 5:28 PM To: Jason Hu Cc: types-list at LISTS.SEAS.UPENN.EDU Subject: Re: [TYPES] reference request: MLTT with Russell's non-cumulative universes Hi Jason! If I understand correctly, you're looking for a syntactic proof of uniqueness of types, and the crucial property you need to make progress here is injectivity of the Pi type constructor (Pi-injectivity). As usual, the devil is in the details, but if you're happy with a formulation of type theory that 1) only has Pi types and universes, but no Sigma types (aka a pure type system) and 2) treats types and terms up to (untyped) beta-equivalence (no eta-conversions) then Pi-injectivity is relatively easy to prove syntactically (via Church-Rosser). I believe that pure type systems (PTS) are sufficient for expressing the sort of non-cumulative universes you want, and that uniqueness of types holds for the relevant class of PTSs. A nice reference for PTSs is Barendregt's "Lambda calculi with types" (1993) -- the chapter, not the book. See Lemma 5.2.21 (p. 109) for a proof of uniqueness of types (I believe the system you have in mind should indeed be singly-sorted). Since you mentioned Agda: I mechanized the basic meta-theory of PTSs (including Pi-injectivity, but not uniqueness of types) a while ago in Agda. It probably won't type-check using an up-to-date version of Agda, but it might still be useful to get the basic ideas: https://urldefense.com/v3/__https://github.com/sstucki/pts-agda__;!!IBzWLUs!XpsRNnHe2MectpW2xSjPR6jeL3VYpZNpP3Pp67bKzE3fTEp5g-n2GsuiGcG65q7JgV2C3p_8JyaJUSV0MK8WafnTf4iFiJM$ Cheers /Sandro On Mon, Aug 15, 2022 at 10:14 PM Jason Hu wrote: > > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Hi all, > > I am writing to see if anyone has formalized a formulation MLTT with non-cumulative universes. This type theory is useful and interesting and is a foundation for, e.g. Agda. In particular, I would like to see some proofs of some properties like type uniqueness. I saw in many places that people say with non-cumulative universes, every term has a unique type (up to equivalence). However, it does not seem very obvious how to prove it easily by syntactic method. For example, consider function application > > t s : T1 [ s ] and t s : T2 [ s ] > > where [ s ] denotes substitution of the topmost variable only. Now we want to prove T1 [ s ] and T2 [ s ] are equivalent. However, induction on t only shows that for some S1 and S2, such that > > t : (x : S1). T1 and t : (x : S2). T2 ==> : (x : S1). T1 ~ (x : S2). T2 > > where ~ is the definitional equivalence relation, but then we are stuck, because we are not able to show T1 ~ T2 without doing a logical relation argument. > > The type uniqueness property is important to prove the property that every type lives in precisely one universe, where we need another property that also needs logical relations to establish: > > Set i ~ Set j ==> i = j > > Is there any document that systematically looks into non-cumulativity? Many I read only talk about cumulative universes and non-cumulativity seems often elided. > > Thanks, > Jason > From Meven.Bertrand at univ-nantes.fr Wed Aug 17 11:58:16 2022 From: Meven.Bertrand at univ-nantes.fr (Meven LENNON-BERTRAND) Date: Wed, 17 Aug 2022 17:58:16 +0200 Subject: [TYPES] reference request: MLTT with Russell's non-cumulative universes In-Reply-To: References: Message-ID: <1f00ebfd-92b1-f5e4-69b1-e7ba11bb7b07@univ-nantes.fr> Hi Jason, Have you looked into the work of Abel and others (starting with/Decidability of Conversion for Type Theory in Type Theory/ at POPL 2018, with various extensions since, all available on Github )? They only have one universe instead of a full hierarchy, and as far as I can tell only uniqueness of types for neutral terms is proven (here ), but this might still be of interest to you. From what I understand, the key idea to go around your issue with substitution is to define reducibility judgments universally with respect to all substitutions, so as to get a strong enough induction principle. You might also be interested in the strategy taken in the MetaCoq project. The whole development is done in the cumulative setting, but I do not think that any idea in the proof would not carry over if we chose to degenerate cumulativity and take it to be equal to conversion: the key technical property is confluence of reduction, from which many things follow, including injectivity of type constructors. The idea is to make a detour through bidirectional typing. The main three steps are the following: 1) show that if |- t : T then also t infers some T' such that T' <= T (with <= being cumulativity) 2) show that if t infers T', then also |- t : T' 3) show that inferred types are unique (up to conversion, or even a stronger relation: in MetaCoq, we show that they have a common reduct). From this, you get type principality (the equivalent of type uniqueness in the cumulative setting, saying that any typable term has a minimal type). If you want to read more about this, the best source is probably my PhD thesis . Best, Meven LENNON-BERTRAND Doctorant, ?quipe Gallinette ? LS2N ? Universit? de Nantes https://urldefense.com/v3/__http://www.meven.ac__;!!IBzWLUs!Vb4IFWcpXSjUT-97xXI-eN3VNzUlkEDre6l38Mv26CpuKQZmjJORIllYIVB6Xl3Jeix7mFvsQ9rAGo0wvo_B8INVsUyZb6bKcFACUrmXZmo$ Le 16/08/2022 ? 03:12, Jason Hu a ?crit?: > [ The Types Forum,http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Hi Sandro, > > Thanks for your reference. I don?t actually necessarily mean a syntactic proof but is more generally wondering whether these properties have been looked into in details and if so, what is the earliest work. I will definitely look into your PTS mechanization. > > Thanks, > Jason > > From: Sandro Stucki > Sent: Monday, August 15, 2022 5:28 PM > To: Jason Hu > Cc:types-list at LISTS.SEAS.UPENN.EDU > Subject: Re: [TYPES] reference request: MLTT with Russell's non-cumulative universes > > Hi Jason! > > If I understand correctly, you're looking for a syntactic proof of > uniqueness of types, and the crucial property you need to make > progress here is injectivity of the Pi type constructor > (Pi-injectivity). As usual, the devil is in the details, but if you're > happy with a formulation of type theory that 1) only has Pi types and > universes, but no Sigma types (aka a pure type system) and 2) treats > types and terms up to (untyped) beta-equivalence (no eta-conversions) > then Pi-injectivity is relatively easy to prove syntactically (via > Church-Rosser). I believe that pure type systems (PTS) are sufficient > for expressing the sort of non-cumulative universes you want, and that > uniqueness of types holds for the relevant class of PTSs. > > A nice reference for PTSs is Barendregt's "Lambda calculi with types" > (1993) -- the chapter, not the book. See Lemma 5.2.21 (p. 109) for a > proof of uniqueness of types (I believe the system you have in mind > should indeed be singly-sorted). > > Since you mentioned Agda: I mechanized the basic meta-theory of PTSs > (including Pi-injectivity, but not uniqueness of types) a while ago in > Agda. It probably won't type-check using an up-to-date version of > Agda, but it might still be useful to get the basic ideas: > https://urldefense.com/v3/__https://github.com/sstucki/pts-agda__;!!IBzWLUs!XpsRNnHe2MectpW2xSjPR6jeL3VYpZNpP3Pp67bKzE3fTEp5g-n2GsuiGcG65q7JgV2C3p_8JyaJUSV0MK8WafnTf4iFiJM$ > > Cheers > /Sandro > > On Mon, Aug 15, 2022 at 10:14 PM Jason Hu wrote: >> [ The Types Forum,http://lists.seas.upenn.edu/mailman/listinfo/types-list ] >> >> Hi all, >> >> I am writing to see if anyone has formalized a formulation MLTT with non-cumulative universes. This type theory is useful and interesting and is a foundation for, e.g. Agda. In particular, I would like to see some proofs of some properties like type uniqueness. I saw in many places that people say with non-cumulative universes, every term has a unique type (up to equivalence). However, it does not seem very obvious how to prove it easily by syntactic method. For example, consider function application >> >> t s : T1 [ s ] and t s : T2 [ s ] >> >> where [ s ] denotes substitution of the topmost variable only. Now we want to prove T1 [ s ] and T2 [ s ] are equivalent. However, induction on t only shows that for some S1 and S2, such that >> >> t : (x : S1). T1 and t : (x : S2). T2 ==> : (x : S1). T1 ~ (x : S2). T2 >> >> where ~ is the definitional equivalence relation, but then we are stuck, because we are not able to show T1 ~ T2 without doing a logical relation argument. >> >> The type uniqueness property is important to prove the property that every type lives in precisely one universe, where we need another property that also needs logical relations to establish: >> >> Set i ~ Set j ==> i = j >> >> Is there any document that systematically looks into non-cumulativity? Many I read only talk about cumulative universes and non-cumulativity seems often elided. >> >> Thanks, >> Jason >> From jkoppel at mit.edu Sat Aug 20 00:07:38 2022 From: jkoppel at mit.edu (Jimmy Koppel) Date: Sat, 20 Aug 2022 00:07:38 -0400 Subject: [TYPES] Type theory of file formats Message-ID: There?s a beautiful fact, not often discussed, that the theory of subtyping explains forwards compatibility between file formats. For example here?s a simple file format for images: type header_length_v1 = {x : uint32 | x >= 2} type width = uint32 type height = uint32 type header_v1(n) = width * height * uint32[n-2] type image_data = uint32[] type image_file_v1 = {n: header_length_v1} * header_v1(n) * image_data This type allows for arbitrary extensions to the header, so that any extension to this format which adds more header fields is a subtype. A reader for this file format is thus forwards-compatible with any format extension which adds more header fields. However, even though I wrote it them above as products, the components of a binary file format are not products. In particular, they do not allow nesting, e.g.: (a*b*c)*d is not compatible with (a*b)*d. Compatibility between two binary formats is determined by the same data being in ?the same place.? Even though, classically, uint32 * uint8 is a subtype of uint32, one could not replace width in the type above with (uint32 * uint8), as that would move the location of the height from bytes 8-11 to bytes 9-12, breaking existing code. For my class, I made up a ?flat sequence type? to describe file formats, which effectively functions as a product type which must be right-associated. I would instead write the header(n) type as width ++ height ++ uint32[n-2]. I have not worked out all the theory, but I?ve noticed fewer students making mistakes about binary compatibly since introducing this idea. Can anyone point me to related work? Yours, Jimmy Koppel MIT CSAIL From jkoppel at mit.edu Sun Aug 21 21:47:04 2022 From: jkoppel at mit.edu (Jimmy Koppel) Date: Sun, 21 Aug 2022 21:47:04 -0400 Subject: [TYPES] Type theory of file formats In-Reply-To: <87y1vhzr45.fsf@nita.mail-host-address-is-not-set> References: <87y1vhzr45.fsf@nita.mail-host-address-is-not-set> Message-ID: On Sun, Aug 21, 2022 at 9:03 AM Christopher League < christopher.league at liu.edu> wrote: > > Hi Jimmy, > > I recognize something much like this as "row types" or "row > polymorphism". I encountered the idea in R?my and Vouillon POPL 97, > Objective ML. > > Interestingly, with row variables, the capability isn't quite modeled as > subtyping but rather *parametric* polymorphism of the extension of the > record type. > > Combining the two can be interesting, and there are probably some > object-modeling papers that do it: subtyping for "depth" extensibility, and > rows for "flat" extensions. To represent objects with subtyping but retain > efficient, flat (non-boxed) in-memory representation was the goal. That > seems similar to your forward-compatible binary file format use case, > though of course some other challenges could arise too! > > Hope that helps, and good luck. > > CL > Hi Chris, (You seem to have replied to just me, but I'll assume that's a mistake.) This is a good connection that I hadn't made before; thank you. Row types look to have more in common with extensibility of JSON formats, which is much easier to do, and much easier to model. I'm still hoping to find some type theory that actually cares about indexes into a byte array. > > Jimmy Koppel writes: > > > > > [ The Types Forum, > https://urldefense.com/v3/__http://lists.seas.upenn.edu/mailman/listinfo/types-list__;!!DeIc-uvKXH9G!-FSN5V0yiQnRrDfBehDbLji9VJVqftqzIlLIBOjjFe8MTrsS8N_FjfXHL2ytBS4UpGbubf-tZBHE9w1inF6SMi0$ > ] > > > > There?s a beautiful fact, not often discussed, that the theory of > subtyping > > explains forwards compatibility between file formats. > > > > > > For example here?s a simple file format for images: > > > > > > type header_length_v1 = {x : uint32 | x >= 2} > > > > type width = uint32 > > > > type height = uint32 > > > > type header_v1(n) = width * height * uint32[n-2] > > > > type image_data = uint32[] > > > > > > type image_file_v1 = {n: header_length_v1} * header_v1(n) * image_data > > > > > > > > This type allows for arbitrary extensions to the header, so that any > > extension to this format which adds more header fields is a subtype. A > > reader for this file format is thus forwards-compatible with any format > > extension which adds more header fields. > > > > > > However, even though I wrote it them above as products, the components > of a > > binary file format are not products. In particular, they do not allow > > nesting, e.g.: (a*b*c)*d is not compatible with (a*b)*d. Compatibility > > between two binary formats is determined by the same data being in ?the > > same place.? Even though, classically, uint32 * uint8 is a subtype of > > uint32, one could not replace width in the type above with (uint32 * > uint8), > > as that would move the location of the height from bytes 8-11 to bytes > > 9-12, breaking existing code. > > > > > > For my class, I made up a ?flat sequence type? to describe file formats, > > which effectively functions as a product type which must be > > right-associated. I would instead write the header(n) type as width ++ > > height ++ uint32[n-2]. I have not worked out all the theory, but I?ve > > noticed fewer students making mistakes about binary compatibly since > > introducing this idea. > > > > > > Can anyone point me to related work? > > > > > > Yours, > > > > Jimmy Koppel > > > > MIT CSAIL > -- Jimmy Koppel twitter.com/jimmykoppel https://urldefense.com/v3/__http://www.jameskoppelcoaching.com__;!!IBzWLUs!S4wpNwoe6w2Q7s9z-HapvFj1KoePa4YHN2QBxnFvwP6rg1O-gEHM8dt2LBxLC7LRGAkE5d947CNiDqY20kikLkJypQWF$ From kthielen at gmail.com Mon Aug 22 01:03:24 2022 From: kthielen at gmail.com (Kalani Thielen) Date: Mon, 22 Aug 2022 01:03:24 -0400 Subject: [TYPES] Type theory of file formats In-Reply-To: References: Message-ID: Hi Jimmy, I?ve used a similar observation in this PL/compiler that I made for Morgan Stanley a few years back: https://urldefense.com/v3/__https://github.com/morganstanley/hobbes__;!!IBzWLUs!Xn2Ulm5-C0403pcAOa7dzz_fxK-N1RaBDiDdLrQw0Gu9jezqnv25nAd6bchH-X7ZWeQD3y-fuvItutbVnbCfS5s6VVK1$ ? although I didn?t require strict field placement but just convertibility as determined by structural subtyping. So e.g. ?{x:int,y:int,z:int}? is a subtype of ?{z:long,x:double}? as witnessed by an inferred function that drops ?y?, swaps ?x? and ?z? while widening them into their respective types. As a special case it optimizes for ?trivial convertibility? (where the supertype is a prefix of the subtype) and the identity function is inferred. There?s a flipped rule for sum types, where it?s always safe to convert into a large subsuming sum (hence the type 0 as the subtype for all types and 1 as the supertype for all types). In this PL, I defined those rules as a system of type classes (ala Haskell), with the additional feature that constraints on qualified types are always eliminated at compile-time (since where this is used at Morgan Stanley, runtime performance penalties have to be minimized). As well as being used to decide compatibility between file formats, this method is also useful to decide compatibility between independent message passing processes. Previously at Morgan Stanley, we had a lot of software that kept ?version numbers? and it could be very difficult to figure out if two ?versions? of a message format could be used together (or on a larger scale, if a whole system was even coherent and ready to trade the next day). Structural subtyping makes that problem much simpler, and also gives you a straightforward explanation for why e.g. two programs can?t communicate. Also on the subject of file formats, beyond just ?flat headers?, I found dependent sum types very useful to make ?file references? as e.g. ?T at f? is an offset in the file ?f? (dynamically determined) where a ?T? value can be found (which, if you mmap a large file, you still need to resolve outside of the file contents since different programs will map at different base addresses). With this it?s easy to build regular recursive types and give type assignments to e.g. btrees and skip lists, decide subtyping on indexes this way, etc. I also added probability distributions to structured types, so again requiring inference of a subtyping witness between convertible structures with different expectations, and used those expectations to encode structures down to their entropy limit ? so that we can minimally store billions of ticks split out by symbol in a skip list and efficiently read them out of mapped files concurrently, automatically converting into a few different types for reporting tools and ad-hoc queries. Hope this helps! > On Aug 20, 2022, at 12:07 AM, Jimmy Koppel wrote: > > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > There?s a beautiful fact, not often discussed, that the theory of subtyping > explains forwards compatibility between file formats. > > > For example here?s a simple file format for images: > > > type header_length_v1 = {x : uint32 | x >= 2} > > type width = uint32 > > type height = uint32 > > type header_v1(n) = width * height * uint32[n-2] > > type image_data = uint32[] > > > type image_file_v1 = {n: header_length_v1} * header_v1(n) * image_data > > > > This type allows for arbitrary extensions to the header, so that any > extension to this format which adds more header fields is a subtype. A > reader for this file format is thus forwards-compatible with any format > extension which adds more header fields. > > > However, even though I wrote it them above as products, the components of a > binary file format are not products. In particular, they do not allow > nesting, e.g.: (a*b*c)*d is not compatible with (a*b)*d. Compatibility > between two binary formats is determined by the same data being in ?the > same place.? Even though, classically, uint32 * uint8 is a subtype of > uint32, one could not replace width in the type above with (uint32 * uint8), > as that would move the location of the height from bytes 8-11 to bytes > 9-12, breaking existing code. > > > For my class, I made up a ?flat sequence type? to describe file formats, > which effectively functions as a product type which must be > right-associated. I would instead write the header(n) type as width ++ > height ++ uint32[n-2]. I have not worked out all the theory, but I?ve > noticed fewer students making mistakes about binary compatibly since > introducing this idea. > > > Can anyone point me to related work? > > > Yours, > > Jimmy Koppel > > MIT CSAIL From jkoppel at mit.edu Mon Aug 22 04:01:30 2022 From: jkoppel at mit.edu (Jimmy Koppel) Date: Mon, 22 Aug 2022 04:01:30 -0400 Subject: [TYPES] Type theory of file formats In-Reply-To: References: Message-ID: This is cool! Can you point me to relevant parts of the repo with examples? On Mon, Aug 22, 2022 at 1:03 AM Kalani Thielen wrote: > Hi Jimmy, > > I?ve used a similar observation in this PL/compiler that I made for Morgan > Stanley a few years back: > https://urldefense.com/v3/__https://github.com/morganstanley/hobbes__;!!IBzWLUs!WAhCjaIxpVfUqykQo-tm_T17e9eXap8gH814S1Bs3-XuAVaYnKFOUf-oUA4tNwSkQq5IKR7_9ZrTBo2NETIYGQI-xJ68$ > > ? although I didn?t require strict field placement but just convertibility > as determined by structural subtyping. So e.g. ?{x:int,y:int,z:int}? is a > subtype of ?{z:long,x:double}? as witnessed by an inferred function that > drops ?y?, swaps ?x? and ?z? while widening them into their respective > types. As a special case it optimizes for ?trivial convertibility? (where > the supertype is a prefix of the subtype) and the identity function is > inferred. There?s a flipped rule for sum types, where it?s always safe to > convert into a large subsuming sum (hence the type 0 as the subtype for all > types and 1 as the supertype for all types). > > In this PL, I defined those rules as a system of type classes (ala > Haskell), with the additional feature that constraints on qualified types > are always eliminated at compile-time (since where this is used at Morgan > Stanley, runtime performance penalties have to be minimized). > > As well as being used to decide compatibility between file formats, this > method is also useful to decide compatibility between independent message > passing processes. Previously at Morgan Stanley, we had a lot of software > that kept ?version numbers? and it could be very difficult to figure out if > two ?versions? of a message format could be used together (or on a larger > scale, if a whole system was even coherent and ready to trade the next > day). Structural subtyping makes that problem much simpler, and also gives > you a straightforward explanation for why e.g. two programs can?t > communicate. > > Also on the subject of file formats, beyond just ?flat headers?, I found > dependent sum types very useful to make ?file references? as e.g. ?T at f? > is an offset in the file ?f? (dynamically determined) where a ?T? value can > be found (which, if you mmap a large file, you still need to resolve > outside of the file contents since different programs will map at different > base addresses). With this it?s easy to build regular recursive types and > give type assignments to e.g. btrees and skip lists, decide subtyping on > indexes this way, etc. > > I also added probability distributions to structured types, so again > requiring inference of a subtyping witness between convertible structures > with different expectations, and used those expectations to encode > structures down to their entropy limit ? so that we can minimally store > billions of ticks split out by symbol in a skip list and efficiently read > them out of mapped files concurrently, automatically converting into a few > different types for reporting tools and ad-hoc queries. > > Hope this helps! > > > > > On Aug 20, 2022, at 12:07 AM, Jimmy Koppel wrote: > > > > [ The Types Forum, > http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > > > There?s a beautiful fact, not often discussed, that the theory of > subtyping > > explains forwards compatibility between file formats. > > > > > > For example here?s a simple file format for images: > > > > > > type header_length_v1 = {x : uint32 | x >= 2} > > > > type width = uint32 > > > > type height = uint32 > > > > type header_v1(n) = width * height * uint32[n-2] > > > > type image_data = uint32[] > > > > > > type image_file_v1 = {n: header_length_v1} * header_v1(n) * image_data > > > > > > > > This type allows for arbitrary extensions to the header, so that any > > extension to this format which adds more header fields is a subtype. A > > reader for this file format is thus forwards-compatible with any format > > extension which adds more header fields. > > > > > > However, even though I wrote it them above as products, the components > of a > > binary file format are not products. In particular, they do not allow > > nesting, e.g.: (a*b*c)*d is not compatible with (a*b)*d. Compatibility > > between two binary formats is determined by the same data being in ?the > > same place.? Even though, classically, uint32 * uint8 is a subtype of > > uint32, one could not replace width in the type above with (uint32 * > uint8), > > as that would move the location of the height from bytes 8-11 to bytes > > 9-12, breaking existing code. > > > > > > For my class, I made up a ?flat sequence type? to describe file formats, > > which effectively functions as a product type which must be > > right-associated. I would instead write the header(n) type as width ++ > > height ++ uint32[n-2]. I have not worked out all the theory, but I?ve > > noticed fewer students making mistakes about binary compatibly since > > introducing this idea. > > > > > > Can anyone point me to related work? > > > > > > Yours, > > > > Jimmy Koppel > > > > MIT CSAIL > > -- Jimmy Koppel twitter.com/jimmykoppel https://urldefense.com/v3/__http://www.jameskoppelcoaching.com__;!!IBzWLUs!WAhCjaIxpVfUqykQo-tm_T17e9eXap8gH814S1Bs3-XuAVaYnKFOUf-oUA4tNwSkQq5IKR7_9ZrTBo2NETIYGZRG-er8$ From kthielen at gmail.com Tue Aug 23 18:49:19 2022 From: kthielen at gmail.com (Kalani Thielen) Date: Tue, 23 Aug 2022 18:49:19 -0400 Subject: [TYPES] Type theory of file formats In-Reply-To: References: Message-ID: <94950804-F9C5-4C82-B24C-63D9F7DA529E@gmail.com> Hi Jimmy, Sure, there are rules for ?safe casting and convertibility? here, specified as type class instances for a function ?convert? that is the (overloaded) witness I mentioned: https://urldefense.com/v3/__https://github.com/morganstanley/hobbes/blob/main/lib/hobbes/boot/convert.hob*L117__;Iw!!IBzWLUs!W0-zeo1mM6947wq87xxjMbmdzG_HUTmO2vfGyyyS014zuZ946KwO0kyiw6P9j9o2z4PaqRYZlEym0mnhUHPhrvp9rTGd$ The syntax is a little unusual, I took some inspiration from Mark Jones?s TREX (as well, inspiration for the implementation of qualified types here from his dissertation on the topic, though as mentioned before not the ?dictionary passing? interpretation but a ?compile-time rewriting? instead). e.g. the highlighted definition above looks like: instance (r={lbl:h*t}, s/lbl :: x, ConvertInto x h, ConvertInto s t) => ConvertInto s r where [?] The constraint ?r={lbl:h*t}? says in English, ?the type ?r? is a non-empty record type whose first field has a name ?lbl? of type ?h?, with the rest of the record as ?t??, then ?s/lbl :: x? says ?the type ?s? can be indexed by ?lbl? to yield a type ?x?? and blah blah blah, so you wind up deriving the function described before to select each of the necessary fields from the source into the destination type. There are also rules for ?castability? as a preferred condition for ?convertibility? as e.g.: https://urldefense.com/v3/__https://github.com/morganstanley/hobbes/blob/main/lib/hobbes/boot/convert.hob*L68__;Iw!!IBzWLUs!W0-zeo1mM6947wq87xxjMbmdzG_HUTmO2vfGyyyS014zuZ946KwO0kyiw6P9j9o2z4PaqRYZlEym0mnhUHPhrhZVynGF$ instance (ar={lbl:ah*at}, br={lbl:bh*()}, Castable ah bh) => Castable ar br where [?] Where the ?from? type ?ar? and the ?to? type ?br? share an exact common prefix up to the final field, which merely has to be castable. The unit type is written ?()? here like in Haskell and is the terminal case for generically splitting record types into heads/tails this way. If you?re interested, there?s a shell that?s part of the project here and you can interact with this overloaded function, which is maybe easier than reading the ?boot? code here: $ hi -s > :t {a={x=1,y=2,z=3}, b={x=1,z=3}, c={y=2}} { a:{ x:int, y:int, z:int }, b:{ x:int, z:int }, c:{ y:int } } > :t convert({a={x=1,y=2,z=3}, b={x=1,z=3}, c={y=2}}) :: {b:{z:double}, a:{z:double,x:long}} { b:{ z:double }, a:{ z:double, x:long } } > convert({a={x=1,y=2,z=3}, b={x=1,z=3}, c={y=2}}) :: {b:{z:double}, a:{z:double,x:long}} {b={z=3}, a={z=3, x=1}} The code for entropy coding ?biased structured types? (types as probabilities?) is here, it?s a header-only C++ lib but it writes in this file format I mentioned where we also do this kind of structural subtyping (compression levels wind up being about the same or better than LZMA for our high volume tick data, but much more practical for our data sets given how much faster this method is): https://urldefense.com/v3/__https://github.com/morganstanley/hobbes/blob/main/include/hobbes/cfregion.H__;!!IBzWLUs!W0-zeo1mM6947wq87xxjMbmdzG_HUTmO2vfGyyyS014zuZ946KwO0kyiw6P9j9o2z4PaqRYZlEym0mnhUHPhrnMfYDkX$ (That code is actually a little out of date from where it has grown inside of Morgan Stanley, but it does work and the basic idea is still the same.) HTH > On Aug 22, 2022, at 4:01 AM, Jimmy Koppel wrote: > > This is cool! Can you point me to relevant parts of the repo with examples? > > On Mon, Aug 22, 2022 at 1:03 AM Kalani Thielen > wrote: > Hi Jimmy, > > I?ve used a similar observation in this PL/compiler that I made for Morgan Stanley a few years back: > https://urldefense.com/v3/__https://github.com/morganstanley/hobbes__;!!IBzWLUs!W0-zeo1mM6947wq87xxjMbmdzG_HUTmO2vfGyyyS014zuZ946KwO0kyiw6P9j9o2z4PaqRYZlEym0mnhUHPhrlqaUequ$ > > ? although I didn?t require strict field placement but just convertibility as determined by structural subtyping. So e.g. ?{x:int,y:int,z:int}? is a subtype of ?{z:long,x:double}? as witnessed by an inferred function that drops ?y?, swaps ?x? and ?z? while widening them into their respective types. As a special case it optimizes for ?trivial convertibility? (where the supertype is a prefix of the subtype) and the identity function is inferred. There?s a flipped rule for sum types, where it?s always safe to convert into a large subsuming sum (hence the type 0 as the subtype for all types and 1 as the supertype for all types). > > In this PL, I defined those rules as a system of type classes (ala Haskell), with the additional feature that constraints on qualified types are always eliminated at compile-time (since where this is used at Morgan Stanley, runtime performance penalties have to be minimized). > > As well as being used to decide compatibility between file formats, this method is also useful to decide compatibility between independent message passing processes. Previously at Morgan Stanley, we had a lot of software that kept ?version numbers? and it could be very difficult to figure out if two ?versions? of a message format could be used together (or on a larger scale, if a whole system was even coherent and ready to trade the next day). Structural subtyping makes that problem much simpler, and also gives you a straightforward explanation for why e.g. two programs can?t communicate. > > Also on the subject of file formats, beyond just ?flat headers?, I found dependent sum types very useful to make ?file references? as e.g. ?T at f? is an offset in the file ?f? (dynamically determined) where a ?T? value can be found (which, if you mmap a large file, you still need to resolve outside of the file contents since different programs will map at different base addresses). With this it?s easy to build regular recursive types and give type assignments to e.g. btrees and skip lists, decide subtyping on indexes this way, etc. > > I also added probability distributions to structured types, so again requiring inference of a subtyping witness between convertible structures with different expectations, and used those expectations to encode structures down to their entropy limit ? so that we can minimally store billions of ticks split out by symbol in a skip list and efficiently read them out of mapped files concurrently, automatically converting into a few different types for reporting tools and ad-hoc queries. > > Hope this helps! > > > > > On Aug 20, 2022, at 12:07 AM, Jimmy Koppel > wrote: > > > > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > > > There?s a beautiful fact, not often discussed, that the theory of subtyping > > explains forwards compatibility between file formats. > > > > > > For example here?s a simple file format for images: > > > > > > type header_length_v1 = {x : uint32 | x >= 2} > > > > type width = uint32 > > > > type height = uint32 > > > > type header_v1(n) = width * height * uint32[n-2] > > > > type image_data = uint32[] > > > > > > type image_file_v1 = {n: header_length_v1} * header_v1(n) * image_data > > > > > > > > This type allows for arbitrary extensions to the header, so that any > > extension to this format which adds more header fields is a subtype. A > > reader for this file format is thus forwards-compatible with any format > > extension which adds more header fields. > > > > > > However, even though I wrote it them above as products, the components of a > > binary file format are not products. In particular, they do not allow > > nesting, e.g.: (a*b*c)*d is not compatible with (a*b)*d. Compatibility > > between two binary formats is determined by the same data being in ?the > > same place.? Even though, classically, uint32 * uint8 is a subtype of > > uint32, one could not replace width in the type above with (uint32 * uint8), > > as that would move the location of the height from bytes 8-11 to bytes > > 9-12, breaking existing code. > > > > > > For my class, I made up a ?flat sequence type? to describe file formats, > > which effectively functions as a product type which must be > > right-associated. I would instead write the header(n) type as width ++ > > height ++ uint32[n-2]. I have not worked out all the theory, but I?ve > > noticed fewer students making mistakes about binary compatibly since > > introducing this idea. > > > > > > Can anyone point me to related work? > > > > > > Yours, > > > > Jimmy Koppel > > > > MIT CSAIL > > > > -- > Jimmy Koppel > twitter.com/jimmykoppel > https://urldefense.com/v3/__http://www.jameskoppelcoaching.com__;!!IBzWLUs!W0-zeo1mM6947wq87xxjMbmdzG_HUTmO2vfGyyyS014zuZ946KwO0kyiw6P9j9o2z4PaqRYZlEym0mnhUHPhrpm6fOOE$ From jkoppel at mit.edu Wed Aug 24 03:21:14 2022 From: jkoppel at mit.edu (Jimmy Koppel) Date: Wed, 24 Aug 2022 03:21:14 -0400 Subject: [TYPES] Type theory of file formats In-Reply-To: <94950804-F9C5-4C82-B24C-63D9F7DA529E@gmail.com> References: <94950804-F9C5-4C82-B24C-63D9F7DA529E@gmail.com> Message-ID: Thanks everyone for the links! This is great stuff, and it will take me a while to look through everything. I'm slightly ashamed for not thinking of Narcissus, having visited Benjamin at Purdue while it was in submission. I'll in particular follow up with Henry and Frank privately, as their work seems especially relevant. On Tue, Aug 23, 2022 at 6:49 PM Kalani Thielen wrote: > Hi Jimmy, > > Sure, there are rules for ?safe casting and convertibility? here, > specified as type class instances for a function ?convert? that is the > (overloaded) witness I mentioned: > > https://urldefense.com/v3/__https://github.com/morganstanley/hobbes/blob/main/lib/hobbes/boot/convert.hob*L117__;Iw!!IBzWLUs!XlDKvMF0Rtlm8BY6LF70llbprMX_mzi-SWRHtZeLm1Hecw_ZL4m5moYgxhcK81vMnvy4TlxIOZhS961qp68yDS_fn-xq$ > > The syntax is a little unusual, I took some inspiration from Mark Jones?s > TREX (as well, inspiration for the implementation of qualified types here > from his dissertation on the topic, though as mentioned before not the > ?dictionary passing? interpretation but a ?compile-time rewriting? instead). > > e.g. the highlighted definition above looks like: > > instance (r={lbl:h*t}, s/lbl :: x, ConvertInto x h, ConvertInto s t) => > ConvertInto s r where [?] > > > The constraint ?r={lbl:h*t}? says in English, ?the type ?r? is a non-empty > record type whose first field has a name ?lbl? of type ?h?, with the rest > of the record as ?t??, then ?s/lbl :: x? says ?the type ?s? can be indexed > by ?lbl? to yield a type ?x?? and blah blah blah, so you wind up deriving > the function described before to select each of the necessary fields from > the source into the destination type. > > There are also rules for ?castability? as a preferred condition for > ?convertibility? as e.g.: > > https://urldefense.com/v3/__https://github.com/morganstanley/hobbes/blob/main/lib/hobbes/boot/convert.hob*L68__;Iw!!IBzWLUs!XlDKvMF0Rtlm8BY6LF70llbprMX_mzi-SWRHtZeLm1Hecw_ZL4m5moYgxhcK81vMnvy4TlxIOZhS961qp68yDekh7iGa$ > > instance (ar={lbl:ah*at}, br={lbl:bh*()}, Castable ah bh) => Castable ar > br where [?] > > > Where the ?from? type ?ar? and the ?to? type ?br? share an exact common > prefix up to the final field, which merely has to be castable. The unit > type is written ?()? here like in Haskell and is the terminal case for > generically splitting record types into heads/tails this way. > > If you?re interested, there?s a shell that?s part of the project here and > you can interact with this overloaded function, which is maybe easier than > reading the ?boot? code here: > > $ hi -s > > :t {a={x=1,y=2,z=3}, b={x=1,z=3}, c={y=2}} > { a:{ x:int, y:int, z:int }, b:{ x:int, z:int }, c:{ y:int } } > > > :t convert({a={x=1,y=2,z=3}, b={x=1,z=3}, c={y=2}}) :: {b:{z:double}, > a:{z:double,x:long}} > { b:{ z:double }, a:{ z:double, x:long } } > > > convert({a={x=1,y=2,z=3}, b={x=1,z=3}, c={y=2}}) :: {b:{z:double}, > a:{z:double,x:long}} > {b={z=3}, a={z=3, x=1}} > > > The code for entropy coding ?biased structured types? (types as > probabilities?) is here, it?s a header-only C++ lib but it writes in this > file format I mentioned where we also do this kind of structural subtyping > (compression levels wind up being about the same or better than LZMA for > our high volume tick data, but much more practical for our data sets given > how much faster this method is): > > https://urldefense.com/v3/__https://github.com/morganstanley/hobbes/blob/main/include/hobbes/cfregion.H__;!!IBzWLUs!XlDKvMF0Rtlm8BY6LF70llbprMX_mzi-SWRHtZeLm1Hecw_ZL4m5moYgxhcK81vMnvy4TlxIOZhS961qp68yDUwMvzp3$ > > (That code is actually a little out of date from where it has grown inside > of Morgan Stanley, but it does work and the basic idea is still the same.) > > HTH > > > > On Aug 22, 2022, at 4:01 AM, Jimmy Koppel wrote: > > This is cool! Can you point me to relevant parts of the repo with examples? > > On Mon, Aug 22, 2022 at 1:03 AM Kalani Thielen wrote: > >> Hi Jimmy, >> >> I?ve used a similar observation in this PL/compiler that I made for >> Morgan Stanley a few years back: >> https://urldefense.com/v3/__https://github.com/morganstanley/hobbes__;!!IBzWLUs!XlDKvMF0Rtlm8BY6LF70llbprMX_mzi-SWRHtZeLm1Hecw_ZL4m5moYgxhcK81vMnvy4TlxIOZhS961qp68yDcXor8qL$ >> >> ? although I didn?t require strict field placement but just >> convertibility as determined by structural subtyping. So e.g. >> ?{x:int,y:int,z:int}? is a subtype of ?{z:long,x:double}? as witnessed by >> an inferred function that drops ?y?, swaps ?x? and ?z? while widening them >> into their respective types. As a special case it optimizes for ?trivial >> convertibility? (where the supertype is a prefix of the subtype) and the >> identity function is inferred. There?s a flipped rule for sum types, where >> it?s always safe to convert into a large subsuming sum (hence the type 0 as >> the subtype for all types and 1 as the supertype for all types). >> >> In this PL, I defined those rules as a system of type classes (ala >> Haskell), with the additional feature that constraints on qualified types >> are always eliminated at compile-time (since where this is used at Morgan >> Stanley, runtime performance penalties have to be minimized). >> >> As well as being used to decide compatibility between file formats, this >> method is also useful to decide compatibility between independent message >> passing processes. Previously at Morgan Stanley, we had a lot of software >> that kept ?version numbers? and it could be very difficult to figure out if >> two ?versions? of a message format could be used together (or on a larger >> scale, if a whole system was even coherent and ready to trade the next >> day). Structural subtyping makes that problem much simpler, and also gives >> you a straightforward explanation for why e.g. two programs can?t >> communicate. >> >> Also on the subject of file formats, beyond just ?flat headers?, I found >> dependent sum types very useful to make ?file references? as e.g. ?T at f? >> is an offset in the file ?f? (dynamically determined) where a ?T? value can >> be found (which, if you mmap a large file, you still need to resolve >> outside of the file contents since different programs will map at different >> base addresses). With this it?s easy to build regular recursive types and >> give type assignments to e.g. btrees and skip lists, decide subtyping on >> indexes this way, etc. >> >> I also added probability distributions to structured types, so again >> requiring inference of a subtyping witness between convertible structures >> with different expectations, and used those expectations to encode >> structures down to their entropy limit ? so that we can minimally store >> billions of ticks split out by symbol in a skip list and efficiently read >> them out of mapped files concurrently, automatically converting into a few >> different types for reporting tools and ad-hoc queries. >> >> Hope this helps! >> >> >> >> > On Aug 20, 2022, at 12:07 AM, Jimmy Koppel wrote: >> > >> > [ The Types Forum, >> http://lists.seas.upenn.edu/mailman/listinfo/types-list ] >> > >> > There?s a beautiful fact, not often discussed, that the theory of >> subtyping >> > explains forwards compatibility between file formats. >> > >> > >> > For example here?s a simple file format for images: >> > >> > >> > type header_length_v1 = {x : uint32 | x >= 2} >> > >> > type width = uint32 >> > >> > type height = uint32 >> > >> > type header_v1(n) = width * height * uint32[n-2] >> > >> > type image_data = uint32[] >> > >> > >> > type image_file_v1 = {n: header_length_v1} * header_v1(n) * image_data >> > >> > >> > >> > This type allows for arbitrary extensions to the header, so that any >> > extension to this format which adds more header fields is a subtype. A >> > reader for this file format is thus forwards-compatible with any format >> > extension which adds more header fields. >> > >> > >> > However, even though I wrote it them above as products, the components >> of a >> > binary file format are not products. In particular, they do not allow >> > nesting, e.g.: (a*b*c)*d is not compatible with (a*b)*d. Compatibility >> > between two binary formats is determined by the same data being in ?the >> > same place.? Even though, classically, uint32 * uint8 is a subtype of >> > uint32, one could not replace width in the type above with (uint32 * >> uint8), >> > as that would move the location of the height from bytes 8-11 to bytes >> > 9-12, breaking existing code. >> > >> > >> > For my class, I made up a ?flat sequence type? to describe file formats, >> > which effectively functions as a product type which must be >> > right-associated. I would instead write the header(n) type as width ++ >> > height ++ uint32[n-2]. I have not worked out all the theory, but I?ve >> > noticed fewer students making mistakes about binary compatibly since >> > introducing this idea. >> > >> > >> > Can anyone point me to related work? >> > >> > >> > Yours, >> > >> > Jimmy Koppel >> > >> > MIT CSAIL >> >> > > -- > Jimmy Koppel > twitter.com/jimmykoppel > https://urldefense.com/v3/__http://www.jameskoppelcoaching.com__;!!IBzWLUs!XlDKvMF0Rtlm8BY6LF70llbprMX_mzi-SWRHtZeLm1Hecw_ZL4m5moYgxhcK81vMnvy4TlxIOZhS961qp68yDfN7cHWT$ > > > -- Jimmy Koppel twitter.com/jimmykoppel https://urldefense.com/v3/__http://www.jameskoppelcoaching.com__;!!IBzWLUs!XlDKvMF0Rtlm8BY6LF70llbprMX_mzi-SWRHtZeLm1Hecw_ZL4m5moYgxhcK81vMnvy4TlxIOZhS961qp68yDfN7cHWT$ From anstenklev at gmail.com Fri Sep 16 05:28:03 2022 From: anstenklev at gmail.com (=?UTF-8?Q?Ansten_M=C3=B8rch_Klev?=) Date: Fri, 16 Sep 2022 11:28:03 +0200 Subject: [TYPES] =?utf-8?q?Martin-L=C3=B6f_transcriptions?= Message-ID: Readers of this list may be interested in the following webpage, which collects transcriptions of lectures given by Per Martin-L?f between the autumn of 1993 and September 2019: https://urldefense.com/v3/__https://pml.flu.cas.cz/__;!!IBzWLUs!W9669Hupko31CKWJ_8gqYW6ay7B2bD26twQxgHjm8lpqu6hkPToE7jxzG1ZY0gN4G3qa4G4eEUyJ4UpPxLDLhkAQ4-Z0Aao$ From rnrand at gmail.com Thu Dec 1 00:49:51 2022 From: rnrand at gmail.com (Robert Rand) Date: Thu, 01 Dec 2022 05:49:51 -0000 Subject: [TYPES] TaPL Course? Message-ID: Hi, I was wondering who is teaching a programming languages course using Types and Programming Languages? I'm planning on teaching such a course at UChicago this Spring (March - June) and I'm looking for inspiration and suggestions. If you're on the quarter system and/or have material you'd like to share, that's especially welcome! Thanks! Robert From alejandro at diaz-caro.info Sat Dec 17 07:13:35 2022 From: alejandro at diaz-caro.info (=?UTF-8?Q?Alejandro_D=C3=ADaz=2DCaro?=) Date: Sat, 17 Dec 2022 09:13:35 -0300 Subject: [TYPES] TaPL Course? In-Reply-To: References: Message-ID: Hi Robert, I give a course at a degree in programming at Quilmes University, using typed lambda calculus. The webpage and notes (in Spanish) is here: https://urldefense.com/v3/__http://clp.web.unq.edu.ar/apuntes-y-practicas/__;!!IBzWLUs!XAPllmUn3YsWKjEpx23e80cVtUf6jfRHZp_x1BoCh6HDYQI2H6l5-PdbaijzRqcyEpv0KoEUIJVYhC1Mg4-z_tXDECi_9hmGGn4L$ However, the notes are mostly based on the following very nice book: G. Dowek & J.-J. Levy, Introduction to the theory of programming languages, Springer, 2011 Fell free to use the exercises or any material if it suits the topics you plan to cover. Best, Alejandro -- Sent from my mobile (i.e. sorry for the bad autocorrections) El s?b, 17 dic. 2022 05:20, Robert Rand escribi?: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > Hi, > > I was wondering who is teaching a programming languages course using Types > and Programming Languages? I'm planning on teaching such a course at > UChicago this Spring (March - June) and I'm looking for inspiration and > suggestions. If you're on the quarter system and/or have material you'd > like to share, that's especially welcome! > > Thanks! > Robert > From andreasnuyts at gmail.com Mon Dec 19 10:03:33 2022 From: andreasnuyts at gmail.com (Andreas Nuyts) Date: Mon, 19 Dec 2022 16:03:33 +0100 Subject: [TYPES] TaPL Course? In-Reply-To: References: Message-ID: <2bd6b522-6fc2-048e-76f5-e428d97652f2@gmail.com> Dear Robert, We have a Formal Systems course based on TAPL at KU Leuven. In 2 practical sessions, the students learn how to use Agda and in the third, they formalize Typed Arithmetic: https://urldefense.com/v3/__https://github.com/anuyts/agda-sessions__;!!IBzWLUs!VVdQCimkUObVjDW1CI1V2_kcHewEmae7Ry_alrqCQq6XESgAi54MWeKWEj0mO12hy2avYusU0aEvQachzxrmpFnznjbhMvi3JQ$ There's also a course project. It used to be a formalization of various extensions of the STLC but now we're formalizing Web Assembly instead. Best, Andreas Nuyts On 01.12.22 06:49, Robert Rand wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Hi, > > I was wondering who is teaching a programming languages course using Types > and Programming Languages? I'm planning on teaching such a course at > UChicago this Spring (March - June) and I'm looking for inspiration and > suggestions. If you're on the quarter system and/or have material you'd > like to share, that's especially welcome! > > Thanks! > Robert From fp at cs.cmu.edu Tue Dec 20 14:14:54 2022 From: fp at cs.cmu.edu (Frank Pfenning) Date: Tue, 20 Dec 2022 14:14:54 -0500 Subject: [TYPES] TaPL Course? In-Reply-To: References: Message-ID: Hi Robert, You might be interested in the "Types and Programming Languages" course we teach at CMU, for which I have written extensive notes that complement the textbook "Practical Foundations of Programming Languages" by Bob Harper. I also have a small implementation of a core language Lambda (which I am happy to share) so students can write, type-check, and run some concrete examples. The course is specifically designed as a "breadth" course in that it does not presuppose any prior experience in functional programming. - Frank On Sat, Dec 17, 2022 at 3:19 AM Robert Rand wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > Hi, > > I was wondering who is teaching a programming languages course using Types > and Programming Languages? I'm planning on teaching such a course at > UChicago this Spring (March - June) and I'm looking for inspiration and > suggestions. If you're on the quarter system and/or have material you'd > like to share, that's especially welcome! > > Thanks! > Robert > -- Frank Pfenning, Professor Computer Science Department Carnegie Mellon University Pittsburgh, PA 15213-3891 https://urldefense.com/v3/__http://www.cs.cmu.edu/*fp__;fg!!IBzWLUs!XziYgKa-Uuca8ko4fRdlXlt_RzXFJBsybnlrX-d7qMvvr5KsG9NJaW6KIlYKfNHYdOZzVfy3djmP8cHwsVPsMfs$ +1 412 268-6343 GHC 6017 From msspertu at amazon.com Wed Dec 21 13:14:04 2022 From: msspertu at amazon.com (Spertus, Mike) Date: Wed, 21 Dec 2022 18:14:04 +0000 Subject: [TYPES] TaPL Course? Message-ID: <092f0aea213c42a3b50a6f7c5eceb727@amazon.com> Robert and I have discussed this offline, but in case it is of interest to others, I have a GitHub repo that repackages the implementations from the course site as Dune projects and adds a REPL for playing with the type checkers interactively at https://urldefense.com/v3/__https://github.com/mspertus/TAPL__;!!IBzWLUs!WrDNkB_Fzfrh4n4XyZK8KHIa1TZ35D0kDmXEjGRX9gqD8L4mt1_BrWO6vIQhcVCnKYHHEY-fS8kf1hORutvxCPQb-x-0$ . You can use them directly on machines with ocaml and Dune 3 or use the included devfile to create a preconfigured development container if you don't want to mess around with installing prerequisites. The readme includes copious usage instructions. Mike -----Original Message----- From: Types-list On Behalf Of Frank Pfenning Sent: Tuesday, December 20, 2022 1:15 PM To: Robert Rand Cc: Types list Subject: RE: [EXTERNAL][TYPES] TaPL Course? [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] Hi Robert, You might be interested in the "Types and Programming Languages" course we teach at CMU, for which I have written extensive notes that complement the textbook "Practical Foundations of Programming Languages" by Bob Harper. I also have a small implementation of a core language Lambda (which I am happy to share) so students can write, type-check, and run some concrete examples. The course is specifically designed as a "breadth" course in that it does not presuppose any prior experience in functional programming. - Frank On Sat, Dec 17, 2022 at 3:19 AM Robert Rand wrote: > [ The Types Forum, > http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > Hi, > > I was wondering who is teaching a programming languages course using > Types and Programming Languages? I'm planning on teaching such a > course at UChicago this Spring (March - June) and I'm looking for > inspiration and suggestions. If you're on the quarter system and/or > have material you'd like to share, that's especially welcome! > > Thanks! > Robert > -- Frank Pfenning, Professor Computer Science Department Carnegie Mellon University Pittsburgh, PA 15213-3891 https://urldefense.com/v3/__http://www.cs.cmu.edu/*fp__;fg!!IBzWLUs!XziYgKa-Uuca8ko4fRdlXlt_RzXFJBsybnlrX-d7qMvvr5KsG9NJaW6KIlYKfNHYdOZzVfy3djmP8cHwsVPsMfs$ +1 412 268-6343 GHC 6017 From aaronngray.lists at gmail.com Wed Dec 21 15:49:51 2022 From: aaronngray.lists at gmail.com (Aaron Gray) Date: Wed, 21 Dec 2022 20:49:51 +0000 Subject: [TYPES] Looking for the Source Code for the Book Object-Oriented Type Systems. Message-ID: Hi, I am looking for a copy of the accompanying source code for the BOPL Workbench to the book "Object-Oriented Type Systems" by Jans Palsberg and Michael I. Schwartzbach. I have managed to obtain an ex university copy of the book, but unable to find the accompanying source code. Unfortunately this is the case with a lot of the older paper source code assets where the University CS FTP site has been taken down, and the author(s) no longer has a copy or access. Regards, Aaron Gray