[-- Attachment #1: Type: text/plain, Size: 821 bytes --] Bohemian Logical & Philosophical Café Michael Makkai Notions of identity for and in higher dimensional categories. January 26 at 16.00 Prague time (GMT+1) The zoom link is on the webpage: https://bohemianlpc.github.io <https://bohemianlpc.github.io/> Makkai’s abstract is at this link: https://bohemianlpc.github.io/abstracts/Makkai.pdf <https://bohemianlpc.github.io/abstracts/Makkai.pdf> Regards, Steve -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/DFEBDA07-2227-414D-82D4-EF7A403C6E6B%40cmu.edu. [-- Attachment #2: Type: text/html, Size: 1933 bytes --]

[-- Attachment #1: Type: text/plain, Size: 1437 bytes --] Please distribute to undergraduate and master's students and appropriate counsellors and supervisors. We have two fully funded PhD positions for work in type theory at Chalmers/Univ. of Gothenburg. Observe that you will get employed at the Univ. of Gothenburg with full employment benefits (health care, pension, etc). Our research ranges from foundational studies (models, homotopy type theory) to actual implementations of interactive proof systems (Agda). The research group consists, beside myself, of Andreas Abel, Nils Anders Danielsson, Peter Dybjer, Ulf Norell and Christian Sattler. PhD positions usually extend to 5 years, where every year you spend 80% of your time reading courses and working on your research, and 20% on teaching. Deadline for application: February 14th 2021 For information on how to apply and whom to contact if you have further questions please visit this link https://web103.reachmee.com/ext/I005/1035/job?site=7&lang=UK&validator=9b89bead79bb7258ad55c8d75228e5b7&job_id=18601 Best regards, Thierry Coquand -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/1B889378-403D-412F-AEAF-A91C62348D18%40chalmers.se. [-- Attachment #2: Type: text/html, Size: 2406 bytes --]

[-- Attachment #1: Type: text/plain, Size: 3711 bytes --] Sorry for the confusion! I was in a hurry, trying to respect the deadline. It is embarassing! I apologise. André ________________________________ De : homotopytypetheory@googlegroups.com <homotopytypetheory@googlegroups.com> de la part de Joyal, André <joyal.andre@uqam.ca> Envoyé : 8 janvier 2021 14:33 À : Nicola Gambino <N.Gambino@leeds.ac.uk>; homotopytypetheory@googlegroups.com <homotopytypetheory@googlegroups.com> Objet : [HoTT] Re: Second Postdoctoral Research Fellowship at Leeds Dear Nicola, Happy New Years! I hope you are well. I am sending you a reference letter in support of the application of Karol Szumilo to the Research Fellowship EPSMA1027. Best wishes, André PS: I was very busy with all sort of things in December. I hope we will soon get a chance to discuss online. ________________________________ De : homotopytypetheory@googlegroups.com <homotopytypetheory@googlegroups.com> de la part de Nicola Gambino <N.Gambino@leeds.ac.uk> Envoyé : 16 décembre 2020 11:50 À : homotopytypetheory@googlegroups.com <homotopytypetheory@googlegroups.com> Objet : [HoTT] Second Postdoctoral Research Fellowship at Leeds Dear all, The University of Leeds is advertising another 3-year Postdoctoral Research Fellowship, to work with me on the project “Syntax and semantics of 2-dimensional type theories”, funded by the US Air Force Office for Scientific Research: https://jobs.leeds.ac.uk/EPSMA1028 Deadline for applications is January 8th, 2021. This is the same date as for the position that was advertised a couple of weeks ago, which is advertised at https://jobs.leeds.ac.uk/EPSMA1027 Please see the Candidate Brief documents in the pages linked above for details. Two applications are needed if you wish to be considered for both positions. With best regards, Nicola == Dr Nicola Gambino Associate Professor in Pure Mathematics and Director of Research and Innovation School of Mathematics, University of Leeds Web: http://www1.maths.leeds.ac.uk/~pmtng/ -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com<mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com>. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/0F1A9D33-D435-48C8-B04E-0F17FE2063B4%40leeds.ac.uk<https://groups.google.com/d/msgid/HomotopyTypeTheory/0F1A9D33-D435-48C8-B04E-0F17FE2063B4%40leeds.ac.uk?utm_medium=email&utm_source=footer>. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com<mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com>. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/QB1PR01MB2948A7E6C03BA9B76BD35560FDAE0%40QB1PR01MB2948.CANPRD01.PROD.OUTLOOK.COM<https://groups.google.com/d/msgid/HomotopyTypeTheory/QB1PR01MB2948A7E6C03BA9B76BD35560FDAE0%40QB1PR01MB2948.CANPRD01.PROD.OUTLOOK.COM?utm_medium=email&utm_source=footer>. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/QB1PR01MB294821E15FA46C4130235BC1FDAE0%40QB1PR01MB2948.CANPRD01.PROD.OUTLOOK.COM. [-- Attachment #2: Type: text/html, Size: 8428 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 2546 bytes --] Dear Nicola, Happy New Years! I hope you are well. I am sending you a reference letter in support of the application of Karol Szumilo to the Research Fellowship EPSMA1027. Best wishes, André PS: I was very busy with all sort of things in December. I hope we will soon get a chance to discuss online. ________________________________ De : homotopytypetheory@googlegroups.com <homotopytypetheory@googlegroups.com> de la part de Nicola Gambino <N.Gambino@leeds.ac.uk> Envoyé : 16 décembre 2020 11:50 À : homotopytypetheory@googlegroups.com <homotopytypetheory@googlegroups.com> Objet : [HoTT] Second Postdoctoral Research Fellowship at Leeds Dear all, The University of Leeds is advertising another 3-year Postdoctoral Research Fellowship, to work with me on the project “Syntax and semantics of 2-dimensional type theories”, funded by the US Air Force Office for Scientific Research: https://jobs.leeds.ac.uk/EPSMA1028 Deadline for applications is January 8th, 2021. This is the same date as for the position that was advertised a couple of weeks ago, which is advertised at https://jobs.leeds.ac.uk/EPSMA1027 Please see the Candidate Brief documents in the pages linked above for details. Two applications are needed if you wish to be considered for both positions. With best regards, Nicola == Dr Nicola Gambino Associate Professor in Pure Mathematics and Director of Research and Innovation School of Mathematics, University of Leeds Web: http://www1.maths.leeds.ac.uk/~pmtng/ -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com<mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com>. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/0F1A9D33-D435-48C8-B04E-0F17FE2063B4%40leeds.ac.uk<https://groups.google.com/d/msgid/HomotopyTypeTheory/0F1A9D33-D435-48C8-B04E-0F17FE2063B4%40leeds.ac.uk?utm_medium=email&utm_source=footer>. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/QB1PR01MB2948A7E6C03BA9B76BD35560FDAE0%40QB1PR01MB2948.CANPRD01.PROD.OUTLOOK.COM. [-- Attachment #1.2: Type: text/html, Size: 5537 bytes --] [-- Attachment #2: SzumLeeds.pdf --] [-- Type: application/pdf, Size: 132551 bytes --]

[-- Attachment #1: Type: text/plain, Size: 1420 bytes --] I'm delighted to announce that we are hiring a postdoctoral fellow at Johns Hopkins in homotopy type theory (broadly defined) funded by the AFSOR through their MURI program. I've described the position and the application process on the homotopy type theory blog while the official solicitation is on mathjobs: https://homotopytypetheory.org/2021/01/03/postdoctoral-position-in-hott-at-johns-hopkins-university/ https://www.mathjobs.org/jobs/list/17122 If you are already working in homotopy type theory, then certainly this call for applications is for you, but I'm also open to considering applications from folks working in nearby areas who would be interested in getting into the field, so if you know anyone in this position, please pass this along. Feel free to get in touch if you'd like to discuss, and please send me an email to alert me to your application once it's in. Happy New Year! Emily Riehl -- Associate Professor, Dept. of Mathematics Johns Hopkins University www.math.jhu.edu/~eriehl she/her -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAAjZwAZxfzx7sM54F29tgdmZaGr2Tkhu0PHbfJh9-0eJhB4oGA%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 2493 bytes --]

Dear Colleagues, I am pleased to announce a new online seminar series: the Bohemian Logical & Philosophical Café. The BLPC is a framework for webinars on current topics in a variety of areas, including theoretical computer science, category theory, mathematical logic, and philosophy. We will start the 26th of January at 16.00 Prague time (GMT+1) with our first speaker: Michael Makkai Notions of identity for and in higher dimensional categories. Further speakers will include: Benno van den Berg, Jouko Väänänen, Jiří Rosický, Jeremy Avigad, André Joyal, and Mike Shulman. Please check our webpage periodically for an updated list of speakers: https://bohemianlpc.github.io With best wishes for the New Year, Steve (for the organizers) -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/875AA81D-71EA-41DB-9F1F-71822947B5B2%40cmu.edu.

Please distribute to undergraduate and master's students and appropriate counsellors and supervisors. Note that we have a large group of faculty, postdocs and graduate students with interests involving homotopy theory, (higher) category theory, and homotopy type theory. Graduate Student Positions Department of Mathematics University of Western Ontario London, Ontario, Canada The Department of Mathematics at the University of Western Ontario solicits applications for its MSc and PhD programs. We have up to 20 fully funded positions available, and applicants from any country are welcome. Our faculty members supervise research in a variety of areas: http://www.math.uwo.ca/graduate/supervisors.html The Department of Mathematics is part of the School of Mathematical Sciences: http://uwo.ca/smss/ More information about our program, including the application procedure, is available at http://www.math.uwo.ca/graduate/ Students normally start in September, in which case applications should be complete (including letters of reference and supplementary material) by February 1. Applications received after this deadline will be reviewed as space permits. Early applications are welcome, and we encourage applicants to apply for external scholarships they are eligible for. Please contact math-grad-program@uwo.ca with any questions you may have. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAEXhy3Pc5UnXLUL%3DPJ5HBArpiPzUMC9ECA37Lb_9nb3bUddrmQ%40mail.gmail.com.

[-- Attachment #1: Type: text/plain, Size: 1262 bytes --] Dear all, The University of Leeds is advertising another 3-year Postdoctoral Research Fellowship, to work with me on the project “Syntax and semantics of 2-dimensional type theories”, funded by the US Air Force Office for Scientific Research: https://jobs.leeds.ac.uk/EPSMA1028 Deadline for applications is January 8th, 2021. This is the same date as for the position that was advertised a couple of weeks ago, which is advertised at https://jobs.leeds.ac.uk/EPSMA1027 Please see the Candidate Brief documents in the pages linked above for details. Two applications are needed if you wish to be considered for both positions. With best regards, Nicola == Dr Nicola Gambino Associate Professor in Pure Mathematics and Director of Research and Innovation School of Mathematics, University of Leeds Web: http://www1.maths.leeds.ac.uk/~pmtng/ -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/0F1A9D33-D435-48C8-B04E-0F17FE2063B4%40leeds.ac.uk. [-- Attachment #2: Type: text/html, Size: 2320 bytes --]

[-- Attachment #1: Type: text/plain, Size: 1098 bytes --] [Apologies for multiple postings] Dear friends and colleagues, The School of Mathematics of the University of Leeds is offering a 3-year postdoctoral research fellowship to work on the EPSRC-funded project "“Monoidal bicategories, linear logic and operads” with Marcelo Fiore (University of Cambridge) and me. Further particulars are at http://jobs.leeds.ac.uk/EPSMA1027 The deadline for applications is January 8th, 2021. If you have any queries, please contact us. With best regards, Nicola -- Dr Nicola Gambino Associate Professor in Pure Mathematics and Director of Research and Innovation School of Mathematics, University of Leeds http://www1.maths.leeds.ac.uk/~pmtng/ -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/4BA8342D-4D75-436F-9FEF-5BE8E67373E4%40leeds.ac.uk. [-- Attachment #2: Type: text/html, Size: 2047 bytes --]

[-- Attachment #1: Type: text/plain, Size: 1051 bytes --] Dear all, As previously announced, the memorial conference for Erik Palmgren will be held online, this Thursday–Saturday, 9:00–11:30 and 13:30–16:30 Stockholm time. Full programme and other details are available at http://logic.math.su.se/palmgren-memorial/ . To receive the Zoom links, please register by emailing < palmgren-memorial@math.su.se> with your details, preferably by tomorrow morning. (We aren’t posting the Zoom details publicly, in order to prevent Zoom-bombing etc.) Best wishes, –Peter (for the organising committee) palmgren-memorial@math.su.se http://logic.math.su.se/palmgren-memorial/ -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAAkwb-%3DCKieo%3D1ZENv-B9g2QHv4TJFdg30tn-hBxM2iBJPnCqw%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 1705 bytes --]

[Please forward as appropriate.] The Math Department at Western will be hiring one or more postdocs to start in summer 2021. The application deadline is December 4, 2020. The full ad is available at https://www.mathjobs.org/jobs/UWO/PDF and I have included the text of it below. The Math Department has large research groups working in topology, (higher) category theory, homotopy type theory and related areas. Applicants in these and other areas represented in the department are particularly encouraged to apply. Our department has an active postdoctoral program and a busy seminar schedule. More information about the department and the School of Mathematical and Statistical Sciences are available at https://www.math.uwo.ca/ and https://uwo.ca/smss/ The positions have a reduced teaching load of just two half-courses. A "half-course" is a 13-week course meeting for 3 or 4 hours each week. Note also that the cost of living in (this) London is quite low. Feel free to contact me with questions, or to use math-pos@uwo.ca Dan ------------- The Department of Mathematics at the University of Western Ontario has several postdoctoral positions available, in any area of Mathematics that is represented within the Department. Information about the Department can be found at https://www.math.uwo.ca. Each position has a two-year term with a flexible start date of July 1, 2021. The salary will be $52,000 CDN per year, plus a tax-free research fund of $1,500 per year. The positions will involve teaching two half-courses per year, in addition to research. Candidates should have completed a Ph.D. in July 2018 or later. The filling of these positions is subject to budgetary considerations. All applications should include a cover letter, a curriculum vitae (including publication list), a research statement, teaching statement, and at least three letters of reference. At least one letter of reference should comment on the teaching abilities of the applicant. E-mail inquiries may be sent to math-pos@uwo.ca. Screening of applications will begin on December 5th, 2020, and will continue until all positions are filled. Western University is committed to employment equity and welcomes applications from all qualified women and men, including visible minorities, Aboriginal persons, persons with disabilities, and LGBTQ persons. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/87d00gexca.fsf%40uwo.ca.

[-- Attachment #1: Type: text/plain, Size: 2278 bytes --] The deadline for applications for this fellowship has been extended to December 1. PhD students working on a thesis are encouraged to apply. ************************************************** HoTT Dissertation Fellowship PhD students close to finishing their thesis are invited to apply for a Dissertation Fellowship in Homotopy Type Theory. This fellowship, generously funded by Cambridge Quantum Computing and Ilyas Khan, will provide $18,000 to support a graduate student finishing a dissertation on a topic broadly related to homotopy type theory. For instance, it can be used to fund a semester free from teaching duties, or to extend a PhD period by a few months. Applications are due by November 15, 2020, with decisions to be announced in mid-December; the fellowship period can be any time between January 1, 2021 and June 30, 2022 at the discretion of the applicant. To apply, please send the following: • A research statement of no more than two pages, describing your thesis project and its relationship to homotopy type theory, when you are planning to finish your PhD, and what the money would be used for. Please also mention your current and past sources of support during your PhD, and say a little about your research plans post-graduation. • A current CV. • A letter from your advisor in support of your thesis plan, and confirming that your department will be able to use the money as planned. Application materials should be submitted by email to: HoTTfellowship@gmail.com <mailto:HoTTfellowship@gmail.com> The recipient of the fellowship will be selected by a committee consisting of Steve Awodey, Thierry Coquand, Emily Riehl, and Mike Shulman, and will be announced at: https://homotopytypetheory.org/2020/10/03/hott-dissertation-fellowship/ <https://homotopytypetheory.org/2020/10/03/hott-dissertation-fellowship/> -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/53B83835-08E8-45B1-8A2D-4F504D14358C%40cmu.edu. [-- Attachment #2: Type: text/html, Size: 5072 bytes --]

[-- Attachment #1: Type: text/plain, Size: 1410 bytes --] Dear all, The memorial conference for Erik Palmgren (1963–2019) will take place online, on Thursday 19 – Friday 21 November (rescheduled from May due to the coronavirus). Talks are to include various topics related to Erik’s work and interests, as well as reminiscences of Erik. All talks will be held over Zoom; the sessions will be within 9:00–11:30 Thu/Fri morning, and 13:30–16:30 Thu/Fri/Sat afternoon (Stockholm time / CET / UTC+1). Invited speakers include Douglas Bridges, Hajime Ishihara, Steve Vickers, and Maria Emilia Maietti. A preliminary schedule and other details are available at http://logic.math.su.se/palmgren-memorial/ . If you plan to attend and would like to join the mailing list for further updates (including Zoom links), please let us know by sending your details to palmgren-memorial@math.su.se in advance. Best wishes, –Peter (for the organising committee) palmgren-memorial@math.su.se http://logic.math.su.se/palmgren-memorial/ -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAAkwb-noYteALgqFTOHA01bEQ_ZW3p_eyoD8vGezwK8zDFU0yQ%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 2110 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 765 bytes --] Dear all, The Institute for Logic, Language and Computation (part of the University of Amsterdam) will be hiring an assistant professor in Theoretical Computer Science. The official add is available here: https://ivi.uva.nl/shared/uva/en/vacancies/2020/10/20-647-assistant-professor-theoretical-computer-science.html?origin=dXb5vvhxSni9fe05dSz4fA Best wishes, Benno -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/fd89dad4-f27f-4d87-93a0-a85d4713ea92n%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 1153 bytes --]

It is my pleasure to announce the next talk in the Every proof assistant on-line seminar series. We are starting the Fall season with Anders Mörtberg who will talk about Cubical Agda. With kind regards, Andrej CUBICAL AGDA: A DEPENDENTLY TYPED PROGRAMMING LANGUAGE WITH UNIVALENCE AND HIGHER INDUCTIVE TYPES Anders Mörtberg Stockholm University Thursday, September 17, 2020 15:00 to 16:00 (Central European Summer Time, UTC+2) Location: online at Zoom ID 989 0478 8985, https://zoom.us/j/98904788985 Proof assistant: Cubical Agda, https://github.com/agda/cubical Abstract: The dependently typed programming language Agda has recently been extended with a cubical mode which provides extensionality principles for reasoning about equality, such as function and propositional extensionality. These principles are typically added axiomatically to proof assistants based on dependent type theory which disrupts the constructive properties of these systems. Cubical type theory provides a solution by giving computational meaning to Homotopy Type Theory and Univalent Foundations, in particular to the univalence axiom and higher inductive types. In the talk I will discuss how Agda was extended to a full-blown proof assistant with native support for univalence and a general schema of higher inductive types. I will also show a variety of examples of how to use Cubical Agda in practice to reason about mathematics and computer science. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAB0nkh1qFFEtkb90aj7RBy%2Bf407nJRwjLdWcu8BvMC1N6Z3c7A%40mail.gmail.com.

[-- Attachment #1: Type: text/plain, Size: 2256 bytes --] The Institute of Philosophy of the Czech Academy of Sciences welcomes applications for two full-time postdoc positions. The two postdocs will work within a project led by Ansten Klev on type theory and the philosophy of mathematics. The main aim of the project is to develop a philosophy of mathematics for Martin-Löf type theory. The postdocs will pursue research programmes of their own that in some way contribute to this overall aim. Both positions last for 30 months and will start in January 2021. In the first part of this 5-year project emphasis will be placed on developing an inferentialist meaning theory for mathematical language. We are especially looking for researchers who fit at least one of these two descriptions: 1. You are well acquainted with inferentialism in at least one of its incarnations (proof-theoretic semantics, the Brandom tradition), and you are interested in extending the programme to the language of mathematics. If you are not already familiar with Martin-Löf type theory, you are willing to learn the basics of the system after arriving in Prague. 2. You are well acquainted with the technical aspects of Martin-Löf type theory and are familiar with Martin-Löf's meaning explanations. You might even know some homotopy type theory and have thought about how the meaning explanations fare within that or other extensions of Martin-Löf type theory. A more detailed description of the project is available upon request from Ansten Klev, who will also attend to any questions applicants may have: klev@flu.cas.cz. The deadline for applying is October 15. Applications should be sent to Olga Bažantová: bazantova@flu.cas.cz. The application should consist of a CV and a brief (1-2 pages) description of the research the applicant plans to carry out while in Prague. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAJHZuqZGaZcfb7d8xFpR9Fju_DoRZCxY9EVHNHGUGcve90V_sA%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 2932 bytes --]

Dear all, The Homotopy Type Theory Electronic Seminar Talks (HoTTEST) are returning in Fall 2020. The speakers are: September 10: Guillaume Brunerie and Peter LeFanu Lumsdaine September 24: Jakob von Raumer October 8: Yuki Maehara October 22: Ambrus Kaposi November 5: Nima Rasekh November 19: Pierre Cagne December 3: Jamie Vicary The seminar will meet on alternating Thursdays at 11:30 Eastern. The seminar is open to all, but some prior familiarity with HoTT will be assumed. For updates and instructions how to attend, please see https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html We know you have a choice when it comes to electronic seminars and we thank you for choosing HoTTEST. Best wishes, Dan Christensen Chris Kapulkin -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAEXhy3N6wK8Ywx8gAW6x%3DuvBtvD_JXHw7REtScTTY2DRH3%2BnUw%40mail.gmail.com.

[-- Attachment #1: Type: text/plain, Size: 5646 bytes --] Dear all, the panel discussion below is on the future of conferences and the publication model of computer science, especially compared to maths and other disciplines. This seems very relevant for us, i.e. the HoTT community. Nicolai -------- Forwarded Message -------- Subject: Panel Debate, Wednesday 2 September @ 3pm UTC: "Evolution or Revolution? The Future of Conferences in Theoretical Computer Science" Date: Mon, 17 Aug 2020 22:54:13 +0100 From: Jamie Vicary <jamie.vicary@cl.cam.ac.uk> [TLDR: Panel Debate on the Future of Conferences in TCS -- panel Fong, Kesner, Pierce, Vardi -- join at 3pm UTC on Weds 2 Sep -- zoom.us/j/177472153 -- reply now from academic email address to propose a question -- please circulate this message widely] Dear all, The entire community is invited to participate in a debate on the future of the conference system in theoretical computer science. Organized as a special event as part of the Online Worldwide Seminar on Logic and Semantics (OWLS), this will provide a rare community-wide opportunity for us to consider the strengths and weaknesses of our current system, and consider if we can do better. The scope of the debate is all aspects of our publishing and community traditions, characterised by prestige earned mostly through publication in competitive conferences, and frequent local and international travel. Possible topics for discussion include the need to publish in conferences for career progression, which usually involves burning carbon; wasted author and reviewer effort when good papers are rejected from highly competitive conferences; the extent of our responsibility as a community to respond to climate change; alternative publishing models, like the journal-focussed system used in mathematics; high costs of conference travel and registration; virtual conference advantages, disadvantages and best practice; improving equality, diversity and access; consequences and response to COVID-19; and the role of professional bodies. These topics have many close relationships, and need to be discussed together to gain a full understanding of the issues involved, and how we can move forward. OUR PANEL To discuss these issues, we have an excellent panel with a wide range of relevant experience: - Dr Brendan Fong, MIT (brendanfong.com) is a postdoctoral researcher with considerable experience organizing virtual conferences and seminars (act2020.mit.edu), and an Executive Editor of the new open-access journal Compositionality. - Professor Delia Kesner, University of Paris (irif.fr/~kesner) has served on the Steering Committee of six conferences and workshops, and is currently the SC Chair of FSCD, the most recent iteration of which was organized at short notice as a virtual event (fscd2020.org). - Professor Benjamin Pierce, University of Pennsylvania (cis.upenn.edu/~bcpierce) has served as PC chair of a range of events including POPL and ICFP, and has written powerfully on the need for the computer science community to adapt to the reality of climate change. - Professor Moshe Vardi, Rice University (cs.rice.edu/~vardi) is Senior Editor of the journal Communications of the ACM, and founded the Federated Logic Conference (FLOC). He has long been a vocal commentator on structural problems with computer science publishing. PROPOSE A QUESTION Questions will be asked by members of the community. That means you! Please reply to this email to propose your question, which could raise any issue in scope. **Why not do it right now?** Make sure to use an academic email address. We'll let you know if your question is accepted, and you'll then have the opportunity to ask it during the debate, and to respond to the panel's comments. WHEN AND WHERE The debate will take place on Wednesday 2 September at 3pm UTC, which corresponds to the following times in a range of cities around the world: 8am San Francisco / 10am Houston / 11am Philadelphia / 4pm London / 5pm Paris / 9pm Mumbai / 11pm Beijing / midnight Tokyo / 1am Sydney The event will take place on Zoom at the following address, with no password or registration required: - zoom.us/j/177472153 The debate will be followed by an opportunity to discuss informally with other members of the community in small groups. WEBPAGE This event is organized as part of the OWLS seminar series. For more information, a calendar you can embed into your own, and to sign up for reminder emails, visit the webpage: - https://www.cs.bham.ac.uk/~vicaryjo/owls/ READING Members of the community may enjoy the following articles, related to the topic of the debate. - Lance Fortnow (2009), "Time for Computer Science to Grow Up", https://cacm.acm.org/magazines/2009/8/34492-viewpoint-time-for-computer-science-to-grow-up - Benjamin Pierce, Michael Hicks, Crista Lopes and Jens Palsberg (2020), "Conferences in an Era of Expensive Carbon", https://cacm.acm.org/magazines/2020/3/243024-conferences-in-an-era-of-expensive-carbon - Moshe Vardi (2020), "Publish and Perish", https://cacm.acm.org/magazines/2020/1/241717-publish-and-perish We hope you will join us for the debate. Please forward this message to members of your research group, and others who may be interested to participate. Best wishes, Jamie -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/bc16b3e1-08e0-3152-65bd-595bf42faead%40gmail.com. [-- Attachment #2: Type: text/html, Size: 8736 bytes --]

[-- Attachment #1: Type: text/plain, Size: 6884 bytes --] Hi Alex, Thanks, that is all really cool stuff! It's neat that you can do a similar thing for equality, I hadn't thought that was possible, though it seems obvious to me when spelled out. I actually started off learning Coq trying to formalize an undergraduate group theory class, and got sidetracked by various ways of making associativity less annoying. I was exploring reflexive decision procedures, but it's wonderful to see other approaches to this problem. With regards to your proposed definition of A involutiveBiEquiv B, I don't believe that it is a true definition of equivalence, since biEquiv is not a mere proposition. The definitions with strictly involutive inversion I have seen generally introduce a type in the middle, so A involutiveEquiv B = (C : Type) x (C equiv A) x (C equiv B), which under univalence is equivalent to equiv but can only strictly satisfy one of the two unit equations for composition. Sincerely, - Jasper Hugunin On Mon, Aug 17, 2020 at 6:48 AM alexr...@gmail.com <alexrice73@gmail.com> wrote: > Hi Jasper, > > I have also thought about these sort of structures a bit, and in fact this > sort of "trick" of decomposing something of passing in an equality also > works in a variety of situations where composition involves transitivity of > equality. For example, you might be interested in Martin Escardo's > version of this for equality > <https://www.cs.bham.ac.uk/~mhe/yoneda/yoneda.html> which contains a fair > bit of discussion on the topic. I have also done some work on this sort of > idea related to groups which can be found here > <https://alexarice.github.io/posts/sgtuf/Strict-Group-Theory-UF.html> and > submitted a pull request to agda standard library with a similar idea to > this for quasi-inverses <https://github.com/agda/agda-stdlib/pull/1156>. > > With respect to the questions at the end, I'm afraid I am not aware of any > definition for which inverses are strict and I expect that (2) (at least in > it's full generality) is not possible as this would imply that > \infty-groupoids are equivalent to strict \infty-groupoids. For involution > you could perhaps do a similar trick that is done in category theory > libraries like agda-categories where you store the data for both > directions. More precisely, if we let your definition be called biEquiv > then you could let > > A involutiveBiEquiv B = A biEquiv B x B biEquiv A > > and then let inverting be given by swapping the order of the product. I > believe this should maintain the nice compositional properties of biEquiv > and adds involutive inverses for "free". > > Hope some of this was useful/interesting. > Alex > > On Sunday, 16 August 2020 at 20:08:47 UTC+1 jas...@cs.washington.edu > wrote: > >> I was thinking about various definitions of equivalence, and the various >> equations we could ask them to satisfy up to definitional equality. (They >> are of course all the same when looking at propositional equality.) >> >> Looking at composition, all the definitions of equivalence I have seen >> before satisfy at most one of the two equations id o p = p or p o id = p >> (for p : A equiv B and _o_ composition). >> >> By adapting the definition by bi-invertible maps, we can get a definition >> of equivalence where both the above equations hold, and additionally we get >> definitional associativity (p o q) o r = p o (q o r). >> >> ----- >> >> Recall the bi-invertible map definition of equivalence is >> A equiv B = >> (f : A -> B) x >> (gl : B -> A) x >> (gr : B -> A) x >> (linv : forall a, gl(f(a)) = a) x >> (rinv : forall b, f(gr(b)) = b) >> Then the identity is (id, id, id, refl, refl). >> >> When composing (f1, gl1, gr1, linv1, rinv1) with (f2, gl2, gr2, linv2, >> rinv2), >> we can take f = f1 o f2, gl = gl2 o gl1, gr = gr2 o gr1, but linv and >> rinv require path induction (essentially to compose instantiations of linv1 >> and linv2). Since path composition in an arbitrary type only satisfies one >> of the two unit equations definitionally, I don't believe it is possible to >> satisfy both id o p and p o id for this definition. >> >> However, we can modify the definitions of linv and rinv inspired by the >> symmetric coinductive definition of equivalence (that A equiv B = (f : A -> >> B) x (g : B -> A) x forall a b, (f a = b) equiv (a = g b)). >> >> So we take linv : forall a b, f a = b -> a = gl b, and rinv : forall a b, >> a = gr b -> f a = b. >> >> (Notice that (b : B) x (f a = b) and (a : A) x (a = gr b) are >> contractible, so this definition is equivalent to the bi-invertible map >> definition, and thus a real definition of equivalence.) >> >> Then for the identity, we take linv = rinv = id. >> Thus for composition, we can take linv = linv2 o linv1 and rinv = rinv1 o >> rinv2, and exploit the fact that the identity function is definitionally a >> two-sided unit for function composition. >> >> Q.E.D. >> >> ----- >> >> Has anyone seen this definition or other definitions with this property >> used before? >> >> This definition does not behave particularly nicely with respect to >> inversion. I know a few definitions with definitional involutive inversion, >> and most definitions seem to satisfy id^-1 = id, but I don't think I know >> any definitions where p^-1 o p = id or p o p^-1 = id. >> >> There is such a wide variety of possible choices with respect to the >> definition of equivalence, I am interested in what additional properties we >> can ask of it to narrow down the scope of a "good" definition, and what >> unavoidable trade offs exist. >> Some good properties I am thinking about are: >> 1) Decomposition into (f : A -> B) x isEquiv f >> 2) Definitional groupoid equations. >> Currently (1) seems to be incompatible with involutive inversion, but as >> shown here we can have both (1) and definitional equations for everything >> except inversion. Can we be more greedy? >> >> Sincerely, >> - Jasper Hugunin >> > -- > You received this message because you are subscribed to the Google Groups > "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/02e9d6bd-3ce7-485a-a6e4-cb29ca02abecn%40googlegroups.com > <https://groups.google.com/d/msgid/HomotopyTypeTheory/02e9d6bd-3ce7-485a-a6e4-cb29ca02abecn%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAGTS-a8Ev95e9eop-DSPgDD6e_tCbQJyxfG-qUt15HYgpZ-hgA%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 8604 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 5184 bytes --] Hi Jasper, I have also thought about these sort of structures a bit, and in fact this sort of "trick" of decomposing something of passing in an equality also works in a variety of situations where composition involves transitivity of equality. For example, you might be interested in Martin Escardo's version of this for equality <https://www.cs.bham.ac.uk/~mhe/yoneda/yoneda.html> which contains a fair bit of discussion on the topic. I have also done some work on this sort of idea related to groups which can be found here <https://alexarice.github.io/posts/sgtuf/Strict-Group-Theory-UF.html> and submitted a pull request to agda standard library with a similar idea to this for quasi-inverses <https://github.com/agda/agda-stdlib/pull/1156>. With respect to the questions at the end, I'm afraid I am not aware of any definition for which inverses are strict and I expect that (2) (at least in it's full generality) is not possible as this would imply that \infty-groupoids are equivalent to strict \infty-groupoids. For involution you could perhaps do a similar trick that is done in category theory libraries like agda-categories where you store the data for both directions. More precisely, if we let your definition be called biEquiv then you could let A involutiveBiEquiv B = A biEquiv B x B biEquiv A and then let inverting be given by swapping the order of the product. I believe this should maintain the nice compositional properties of biEquiv and adds involutive inverses for "free". Hope some of this was useful/interesting. Alex On Sunday, 16 August 2020 at 20:08:47 UTC+1 jas...@cs.washington.edu wrote: > I was thinking about various definitions of equivalence, and the various > equations we could ask them to satisfy up to definitional equality. (They > are of course all the same when looking at propositional equality.) > > Looking at composition, all the definitions of equivalence I have seen > before satisfy at most one of the two equations id o p = p or p o id = p > (for p : A equiv B and _o_ composition). > > By adapting the definition by bi-invertible maps, we can get a definition > of equivalence where both the above equations hold, and additionally we get > definitional associativity (p o q) o r = p o (q o r). > > ----- > > Recall the bi-invertible map definition of equivalence is > A equiv B = > (f : A -> B) x > (gl : B -> A) x > (gr : B -> A) x > (linv : forall a, gl(f(a)) = a) x > (rinv : forall b, f(gr(b)) = b) > Then the identity is (id, id, id, refl, refl). > > When composing (f1, gl1, gr1, linv1, rinv1) with (f2, gl2, gr2, linv2, > rinv2), > we can take f = f1 o f2, gl = gl2 o gl1, gr = gr2 o gr1, but linv and > rinv require path induction (essentially to compose instantiations of linv1 > and linv2). Since path composition in an arbitrary type only satisfies one > of the two unit equations definitionally, I don't believe it is possible to > satisfy both id o p and p o id for this definition. > > However, we can modify the definitions of linv and rinv inspired by the > symmetric coinductive definition of equivalence (that A equiv B = (f : A -> > B) x (g : B -> A) x forall a b, (f a = b) equiv (a = g b)). > > So we take linv : forall a b, f a = b -> a = gl b, and rinv : forall a b, > a = gr b -> f a = b. > > (Notice that (b : B) x (f a = b) and (a : A) x (a = gr b) are > contractible, so this definition is equivalent to the bi-invertible map > definition, and thus a real definition of equivalence.) > > Then for the identity, we take linv = rinv = id. > Thus for composition, we can take linv = linv2 o linv1 and rinv = rinv1 o > rinv2, and exploit the fact that the identity function is definitionally a > two-sided unit for function composition. > > Q.E.D. > > ----- > > Has anyone seen this definition or other definitions with this property > used before? > > This definition does not behave particularly nicely with respect to > inversion. I know a few definitions with definitional involutive inversion, > and most definitions seem to satisfy id^-1 = id, but I don't think I know > any definitions where p^-1 o p = id or p o p^-1 = id. > > There is such a wide variety of possible choices with respect to the > definition of equivalence, I am interested in what additional properties we > can ask of it to narrow down the scope of a "good" definition, and what > unavoidable trade offs exist. > Some good properties I am thinking about are: > 1) Decomposition into (f : A -> B) x isEquiv f > 2) Definitional groupoid equations. > Currently (1) seems to be incompatible with involutive inversion, but as > shown here we can have both (1) and definitional equations for everything > except inversion. Can we be more greedy? > > Sincerely, > - Jasper Hugunin > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/02e9d6bd-3ce7-485a-a6e4-cb29ca02abecn%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 6273 bytes --]

[-- Attachment #1: Type: text/plain, Size: 3394 bytes --] I was thinking about various definitions of equivalence, and the various equations we could ask them to satisfy up to definitional equality. (They are of course all the same when looking at propositional equality.) Looking at composition, all the definitions of equivalence I have seen before satisfy at most one of the two equations id o p = p or p o id = p (for p : A equiv B and _o_ composition). By adapting the definition by bi-invertible maps, we can get a definition of equivalence where both the above equations hold, and additionally we get definitional associativity (p o q) o r = p o (q o r). ----- Recall the bi-invertible map definition of equivalence is A equiv B = (f : A -> B) x (gl : B -> A) x (gr : B -> A) x (linv : forall a, gl(f(a)) = a) x (rinv : forall b, f(gr(b)) = b) Then the identity is (id, id, id, refl, refl). When composing (f1, gl1, gr1, linv1, rinv1) with (f2, gl2, gr2, linv2, rinv2), we can take f = f1 o f2, gl = gl2 o gl1, gr = gr2 o gr1, but linv and rinv require path induction (essentially to compose instantiations of linv1 and linv2). Since path composition in an arbitrary type only satisfies one of the two unit equations definitionally, I don't believe it is possible to satisfy both id o p and p o id for this definition. However, we can modify the definitions of linv and rinv inspired by the symmetric coinductive definition of equivalence (that A equiv B = (f : A -> B) x (g : B -> A) x forall a b, (f a = b) equiv (a = g b)). So we take linv : forall a b, f a = b -> a = gl b, and rinv : forall a b, a = gr b -> f a = b. (Notice that (b : B) x (f a = b) and (a : A) x (a = gr b) are contractible, so this definition is equivalent to the bi-invertible map definition, and thus a real definition of equivalence.) Then for the identity, we take linv = rinv = id. Thus for composition, we can take linv = linv2 o linv1 and rinv = rinv1 o rinv2, and exploit the fact that the identity function is definitionally a two-sided unit for function composition. Q.E.D. ----- Has anyone seen this definition or other definitions with this property used before? This definition does not behave particularly nicely with respect to inversion. I know a few definitions with definitional involutive inversion, and most definitions seem to satisfy id^-1 = id, but I don't think I know any definitions where p^-1 o p = id or p o p^-1 = id. There is such a wide variety of possible choices with respect to the definition of equivalence, I am interested in what additional properties we can ask of it to narrow down the scope of a "good" definition, and what unavoidable trade offs exist. Some good properties I am thinking about are: 1) Decomposition into (f : A -> B) x isEquiv f 2) Definitional groupoid equations. Currently (1) seems to be incompatible with involutive inversion, but as shown here we can have both (1) and definitional equations for everything except inversion. Can we be more greedy? Sincerely, - Jasper Hugunin -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAGTS-a9Qo5jTP7bMsHkQGgBp9y46icJ1m1bB0qiSiHUS%2BJxQGw%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 4273 bytes --]

LICS 2020 will include two "HoTT heavy" sessions (B5 on Wednesday July 8 and E5 on Friday July 10). The talks are already online, and participation in the Q/A session will be live via Zoom. Registration is free: https://lics2020.saarland-informatics-campus.de/schedule/ -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/D5AEEB22-F17C-4452-826F-C3F6E16A1972%40cmu.edu.

[-- Attachment #1.1: Type: text/plain, Size: 2517 bytes --] The Compositional Systems and Methods group at the Tallinn University of Technology, Estonia (https://compose.ioc.ee) is seeking highly qualified PhD candidates. The ideal student should have a solid grounding in category theory, and in at least one of the following areas: programming languages, concurrency theory, quantum computing, database and information systems, or machine learning. The group’s lingua franca is category theory and our research concerns mathematical foundations, as well as various applications in computer science and related disciplines. We are working on relational algebra and functorial semantics, open games, process languages for smart contracts, string diagrams, compositional descriptions of models of computation and concurrency, lenses and optics in functional programming, type theory, and several other topics. The group is led by Pawel Sobocinski, has two postdoctoral researchers, Edward Morehouse and Fosco Loregian, and four PhD students: Elena Di Lavore, Nathan Haydon, Chad Nester and Mario Román. One additional postdoctoral researcher will be recruited in the autumn of 2020. Our research is supported by the ESF funded Estonian IT Academy research measure. The group’s ethos emphasises openness, and inter-group collaboration is highly encouraged. We maintain an active member-led seminar series and hold regular group meetings, research retreats in the Estonian countryside, and various cross-cutting research activities. The successful students will be awarded a generous stipend and be provided with computing equipment and resources for travelling to conferences, summer schools, and other events relevant to their projects. Applicants should hold a Masters degree in Computer Science, Mathematics or a closely related field. To apply, send a CV and a motivation letter outlining your research interests to Pawel Sobocinski pawel.sobocinski@taltech.ee. APPLICATION DEADLINE: July 31, 2020 STARTING DATE: November 2020 or as per agreement Fosco Loregian Edward Morehouse Pawel Sobocinski -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/be861f35-c084-47c8-be72-bbf1d17b82e7o%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 2827 bytes --]

CALL FOR PARTICIPATION Workshop on Homotopy Type Theory and Univalent Foundations July 5-7, 2020, The Internet https://hott-uf.github.io/2020 Homotopy Type Theory is a young area of logic, combining ideas from several established fields: the use of dependent type theory as a foundation for mathematics, inspired by ideas and tools from abstract homotopy theory. Univalent Foundations are foundations of mathematics based on the homotopical interpretation of type theory. The goal of this workshop is to bring together researchers interested in all aspects of Homotopy Type Theory and Univalent Foundations: from the study of syntax and semantics of type theory to practical formalization in proof assistants based on univalent type theory. # Registration Registration is free of charge, but required. The details can be found on the event website. # Invited talks * Carlo Angiuli (Carnegie Mellon University) From raw terms to recollement * Liron Cohen (Ben-Gurion University) Building Effectful Realizability Models, Uniformly * Pierre-Louis Curien (Université de Paris) A syntactic approach to opetopes, opetopic sets and opetopic categories # Contributed talks 21 talks were accepted by the Program Committee. Their titles and abstracts are available on the event website. # Schedule The event will take place from July 5-7, 2020. The talks are scheduled between 2 PM and 7:30 PM CEST (UTC+2). Detailed schedule is now available on the website. # Organizers * Benedikt Ahrens (University of Birmingham) * Chris Kapulkin (University of Western Ontario) -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAEXhy3O9E5m4iAkxxX7xMCGHnnsdE71c_nHWvPhNoVKMjtfe_w%40mail.gmail.com.

[-- Attachment #1: Type: text/plain, Size: 4282 bytes --] ===================================== CALL FOR PARTICIPATION Logical Frameworks and Meta-Languages: Theory and Practice<https://lfmtp.org/workshops/2020/program.shtml> LFMTP 2020 On-line conference, ==> 29-30 June 2020 <== Affiliated with FSCD 2020 and IJCAR 2020<https://fscd-ijcar-2020.org/>. The 2020 editions of LFMTP will be held online and it will consists of - 8 regular talks - 2 invited talks by Elaine Pimentel and Andre Popescu Participation will be free, but a preregistration is required to join the video meetings of the events. Registration page<https://fscd-ijcar-2020.org/register> ===================================== ABOUT LFMTP Logical frameworks and meta-languages form a common substrate for representing, implementing and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their design, implementation and their use in reasoning tasks, ranging from the correctness of software to the properties of formal systems, have been the focus of considerable research over the last two decades. This workshop will bring together designers, implementors and practitioners to discuss various aspects impinging on the structure and utility of logical frameworks, including the treatment of variable binding, inductive and co-inductive reasoning techniques and the expressiveness and lucidity of the reasoning process. LFMTP 2020 will provide researchers a forum to present state-of-the-art techniques and discuss progress in areas such as the following: * Encoding and reasoning about the meta-theory of programming languages, process calculi and related formally specified systems. * Formalisation of model-theoretic and proof-theoretic semantics of logics. ABOUT LFMTP Logical frameworks and meta-languages form a common substrate for representing, implementing and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their design, implementation and their use in reasoning tasks, ranging from the correctness of software to the properties of formal systems, have been the focus of considerable research over the last two decades. This workshop will bring together designers, implementors and practitioners to discuss various aspects impinging on the structure and utility of logical frameworks, including the treatment of variable binding, inductive and co-inductive reasoning techniques and the expressiveness and lucidity of the reasoning process. LFMTP 2020 will provide researchers a forum to present state-of-the-art techniques and discuss progress in areas such as the following: * Encoding and reasoning about the meta-theory of programming languages, process calculi and related formally specified systems. * Formalisation of model-theoretic and proof-theoretic semantics of logics. * Applications of logical frameworks: proof-carrying architectures, proof exchange and transformation, program refactoring, etc. * Techniques for programming with binders in functional programming languages such as Haskell, OCaml or Agda, and logic programming languages such as lambda Prolog or Alpha-Prolog. * Design and implementation of systems and tools related to meta-languages and logical frameworks PROGRAM COMMITTEE David Baelde, LSV, ENS Paris-Saclay & Inria Paris Frédéric Blanqui, INRIA Alberto Ciaffaglione, University of Udine Dennis Müller, Friedrich-Alexander-University Erlangen-Nürnberg Michael Norrish, Data61 Carlos Olarte, Universidade Federal do Rio Grande do Norde Claudio Sacerdoti Coen, University of Bologna (PC Co-Chair) Ulrich Schöpp, fortiss GmbH Alwen Tiu, Australian National University (PC Co-Chair) Tjark Weber, Uppsala University -- Prof. Claudio Sacerdoti Coen Department of Computer Science and Engineering University of Bologna -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/1e271a79fb520a5a1d0b62c88580436d049b826a.camel%40unibo.it. [-- Attachment #2: Type: text/html, Size: 6021 bytes --]