Dear colleagues, We are looking to recruit a postdoctoral researcher to work with us at the University of Strathclyde (Glasgow, Scotland) on our EPSRC grant EP/Y000455/1 A Correct-by-Construction Approach to Approximate Computation. This research is aiming at combining techniques from logics, model theory, type theory, category theory, continuous mathematics and AI for developing the foundations of approximate (quantitative) computation and apply this to programming and learning paradigms. More details about the project can be found here: https://personal.cis.strath.ac.uk/r.mardare/projects.htm The call for this position, with a deadline of 31 March, can be found here: https://strathvacancies.engageats.co.uk/Vacancies/W/5820/0/421067/15019/research-fellow-599328 Kind regards, Radu Mardare Neil Ghani Fredrik Nordvall Forsberg -- 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/e21f6403-479c-431d-8a0b-e0e4fa574c40%40strath.ac.uk.
[-- Attachment #1.1: Type: text/plain, Size: 2992 bytes --] [Apologies for multiple postings.] Autumn school "Proof and Computation" Fischbachau, Germany, 15th to 21st September 2024 http://www.mathematik.uni-muenchen.de/~schwicht/pc24.php This year's international autumn school "Proof and Computation" will be held from 15th to 21st September 2024 in Fischbachau near Munich. Its aim is to bring together young researchers in the field of Foundations of Mathematics, Computer Science and Philosophy. SCOPE -------------------- - Predicative Foundations - Constructive Mathematics and Type Theory - Computation in Higher Types - Extraction of Programs from Proofs COURSES -------------------- - Thierry Coquand (Gothenburg): Topos theory and constructive mathematics - Klaus Mainzer (Munich): From Proof and Computation to AI - Logical, Mathematical, and Philosophical Foundations - Gerhard Jäger (Bern): Foundations of explicit mathematics - Sara Negri (Padua): Enriched syntax for enhanced proof theory - Monika Seisenberger (Swansea): Extraction of programs from proofs - Holger Thies (Kyoto): Extracting efficient programs from proofs in analysis - Freek Wiedijk (Nijmegen): The De Bruijn criterion versus the Poincare principle WORKING GROUPS -------------------- There will be an opportunity to form ad-hoc groups working on specific projects, but also to discuss in more general terms the vision of constructing correct programs from proofs. APPLICATIONS -------------------- Graduate or PhD students and young postdoctoral researchers are invited to apply. Applications (e.g. a self-introduction including research interests and motivation) should be sent to Chuangjie Xu <xu@math.lmu.de>. Students are required to provide also a letter of recommendation, preferably from the thesis adviser. Please specify in your application whether you are interested in applying for financial support (details provided below). Deadline for applications: **7th June 2024**. Applicants will be notified by 24th June 2024. FINANCIAL SUPPORT -------------------- Successful applicants are eligible to apply for financial support that covers accommodation and meals for the duration of the autumn school (approximately 116 Euros per day). Please note that there are no funds available for the reimbursement of travel or additional expenses, which successful applicants will need to cover independently. The workshop is supported by the Udo Keller Stiftung (Hamburg) and the COST Action EuroProofNet. Klaus Mainzer Peter Schuster Helmut Schwichtenberg -- 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/1d998bbd-5158-4550-a1dc-4caaa6146062n%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 3536 bytes --]
[-- Attachment #1: Type: text/plain, Size: 4105 bytes --] Tenth Workshop on MATHEMATICALLY STRUCTURED FUNCTIONAL PROGRAMMING Monday 8th July 2024, Tallinn, Estonia A satellite workshop of FSCD 201:5924 https://msfp-workshop.github.io/msfp2024/ ** Deadline: Friday 26th April (abstract), Tuesday 30th April (paper) ** The tenth workshop on Mathematically Structured Functional Programming is devoted to the derivation of functionality from structure. It is a celebration of the direct impact of Theoretical Computer Science on programs as we write them today. Modern programming languages, and in particular functional languages, support the direct expression of mathematical structures, equipping programmers with tools of remarkable power and abstraction. Where would Haskell be without monads? Functional reactive programming without arrows? Call-by-push-value without adjunctions? The list goes on. This workshop is a forum for researchers who seek to reflect mathematical phenomena in data and control. MSFP 2024 will be held on Monday 8th July 2024 in Tallinn, Estonia in affiliation with FSCD (https://compose.ioc.ee/icalp2024/). Previous instances have been held in Munich (with ETAPS 2022), virtually (2020), in Oxford (with FLOC 2018), Eindhoven (with ETAPS 2016), Grenoble (ETAPS 2014), Tallinn (with ETAPS 2012), Baltimore (with ICFP 2010), Reykjavik (with ICALP 2008), and Kuressaare (with MPC and AMAST 2006). Important Dates: ================ Abstract deadline: Friday 26th April (AoE) Paper deadline: Tuesday 30th April (AoE) Notification: Tuesday 4th June (16:00 UTC) Final version: Tuesday 25th June (AoE) Workshop: Monday 8th July Invited Speakers: ================= TBA Programme Committee: ==================== Kazuyuki Asada - Tohoku University, JP Robert Atkey - University of Strathclyde, UK Ana Bove - Chalmers University of Technology, SE Liang-Ting Chen - Academia Sinica, TW Peng Fu - University of South Carolina, US Jeremy Gibbons - University of Oxford, UK (co-chair) Kuen-Bang Hou (Favonia) - University of Minnesota, UK (co-chair) Robin Kaarsgaard - University of Southern Denmark, DK Paul Blain Levy - University of Birmingham, UK Dan Marsden - University of Nottingham, UK Dylan McDermott - Reykjavik University, IS (more to follow) Submission: =========== Submissions are welcomed on, but by no means restricted to, topics such as: structured effectful computation structured recursion structured corecursion structured tree and graph operations structured syntax with variable binding structured datatype-genericity structured search structured representations of functions structured quantum computation structure directed optimizations structured types structure derived from programs and data Please contact the programme chairs Favonia (kbh@umn.edu) and Jeremy Gibbons (jeremy.gibbons@cs.ox.ac.uk) if you have any questions about the scope of the workshop. We accept two categories of submission: full papers of at most 15 pages that will appear in the proceedings (published with EPTCS) and extended abstracts of at most two pages, which we will post on the website but do not constitute formal publications and will not appear in the proceedings. A short abstract should be submitted by four days in advance of the paper deadline (for both full paper and extended abstract submissions). For full details, see the webpage. We are using EasyChair to manage submissions: https://easychair.org/conferences/?conf=msfp2024 -- 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/CAH_%2BrvdkDqsh5n97Ssy%3D-ZdqGsu61tE%3D9Jy6Qez4QHX8ELz%3DxA%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 5207 bytes --]
[-- Attachment #1: Type: text/plain, Size: 5629 bytes --] Call for Contributions -- Deadline Extension TYPES 2024 30th International Conference on Types for Proofs and Programs Copenhagen, Denmark, 10 - 14 June 2024 https://types2024.itu.dk ===============================[ NEWS ]============================== DATES ----- * Submission of abstract 11 March 2024 AoE **NEW** * Author notification 19 April 2024 AoE * Camera-ready version of abstract 10 May 2024 AoE * Conference 10 - 14 June 2024 ACCOMMODATION ------------- We have reserved a number of hotel rooms at reduced rates. Details at https://types2024.itu.dk/Venue.html ===================================================================== OVERVIEW -------- The TYPES meetings are a forum to present new and on-going work in all aspects of type theory and its applications, especially in formalised and computer assisted reasoning and computer programming. The TYPES areas of interest include, but are not limited to: * foundations of type theory and constructive mathematics; * applications of type theory; * dependently typed programming; * industrial uses of type theory technology; * meta-theoretic studies of type systems; * proof assistants and proof technology; * automation in computer-assisted reasoning; * links between type theory and functional programming; * formalizing mathematics using type theory. We encourage talks proposing new ways of applying type theory. In the spirit of workshops, talks may be based on newly published papers, work submitted for publication, but also work in progress. CONTRIBUTED TALKS ----------------- TYPES solicits contributed talks to stimulate discussions. Selection of those will be based on extended abstracts/short papers of 2 pp (not including bibliography) formatted with easychair.cls. Camera-ready versions of the accepted contributions will be published in an informal book of abstracts for distribution during the conference. POST-PROCEEDIGNS ---------------- A post-proceedings volume will be published in the Leibniz International Proceedings in Informatics (LIPIcs) series. Submission to that volume will be open to everyone. Tentative submission deadline for the post-proceedings: October 2024. PROGRAMME COMMITTEE ------------------- Patrick Bahr (IT University of Copenhagen, Denmark) (co-chair) Henning Basold (Leiden University, The Netherlands) Andrej Bauer (University of Ljubljana, Slovenia) Marco Carbone (IT University of Copenhagen, Denmark) Jesper Cockx (TU Delft, The Netherlands) Greta Coraglia (University of Milan, Italy) Peter Dybjer (Chalmers University of Technology, Sweden) Yannick Forster (INRIA, France) Hugo Herbelin (INRIA, France) Patricia Johann (Appalachian State University, USA) Marie Kerjean (CNRS, France) Ekaterina Komendantskaya (University of Southampton, United Kingdom) Meven Lennon-Bertrand (University of Cambridge, United Kingdom) Assia Mahboubi (INRIA, France) Sonia Marin (University of Birmingham, United Kingdom) Anders Mörtberg (Stockholm University, Sweden) Rasmus Ejlers Møgelberg (IT University of Copenhagen, Denmark) (co-chair) Benjamin Pierce (University of Pennsylvania, USA) Jakob Rehof (Technical University of Dortmund, Germany) Simona Ronchi Della Rocca (University of Turin, Italy) Kristina Sojakova (Vrije Universiteit Amsterdam, The Netherlands) Ana Sokolova (University of Salzburg, Austria) Bas Spitters (Aarhus University, Denmark) Wouter Swierstra (Utrecht University, The Netherlands) Philip Wadler (University of Edinburgh, United Kingdom) TYPES STEERING COMMITTEE ------------------------ Sandra Alves (University of Porto, Portugal) Eduardo Hermo Reyes (Formal Vindications, Spain) Rasmus Ejlers Møgelberg (IT University of Copenhagen, Denmark) Paige Randall North (Utrecht University, The Netherlands) (chair) Matthieu Sozeau (INRIA & Université de Nantes, France) Benno van den Berg (University of Amsterdam, The Netherlands) (secretary) ABOUT TYPES ----------- The TYPES meetings from 1990 to 2008 were annual workshops of a sequence of five EU funded networking projects. From 2009 to 2021, TYPES has been run as an independent conference series. Previous TYPES meetings were held in Antibes (1990), Edinburgh (1991), Båstad (1992), Nijmegen (1993), Båstad (1994), Torino (1995), Aussois (1996), Kloster Irsee (1998), Lökeberg (1999), Durham (2000), Berg en Dal near Nijmegen (2002), Torino (2003), Jouy-en-Josas near Paris (2004), Nottingham (2006), Cividale del Friuli (2007), Torino (2008), Aussois (2009), Warsaw (2010), Bergen (2011), Toulouse (2013), Paris (2014), Tallinn (2015), Novi Sad (2016), Budapest (2017), Braga (2018), Oslo (2019), Virtual (2021), Nantes (2022), València (2023). CONTACT ------- Email: types2024@easychair.org ORGANIZERS ---------- Patrick Bahr (IT University of Copenhagen, Denmark) Marco Carbone (IT University of Copenhagen, Denmark) Rasmus Ejlers Møgelberg (IT University of Copenhagen, Denmark) -- 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/CAO0VQQZ_4-Dn%2BpEmw4DfMZYqyvtGd30%2BAeSLDOoV%2BjF5JtVFUA%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 6489 bytes --]
There are just a few days left now to register for this year's Midlands Graduate School (MGS) in Leicester. We offer courses on category theory, proof theory, type theory, session types, and more. 8-12 April 2024, Leicester, UK. Registration closes Friday 8th March. ========================================================== Midlands Graduate School 2024 8-12 April 2024, Leicester, UK https://www.cs.le.ac.uk/events/mgs2024/ BACKGROUND: The Midlands Graduate School (MGS) in the Foundations of Computing Science provides an intensive course of lectures on the mathematical foundations of computing. The MGS has been running since 1999, and is aimed at PhD students in their first or second year of study, but the school is open to everyone, and has increasingly seen participation from industry. We welcome participants from all over the world! COURSES: Seven courses will be given. Participants usually take all the introductory courses and choose additional options from the advanced courses depending on their interests. Guest lecture - Formalisation of Mathematics, Kevin Buzzard Introductory courses - Category Theory, Thorsten Altenkirch - Proof Theory, Abhishek De and Iris van der Giessen - Type Theory with Agda, Todd Ambridge Advanced courses - Session Types, Sonia Marin - Synthetic Homotopy Theory with HoTT/UF, Ulrik Buchholtz - Graph Rewriting, Reiko Heckel - Categorical Realisability, Tom de Jong REGISTRATION: Registration is £295 for students, and £550 for academic, industry and independent participants. The fee includes all lecture courses and example classes, lunch and coffee breaks, and the conference dinner. The registration deadline is ** Friday 8th March **. Spaces are limited, so please register early to secure your place. SPONSORSHIP: We offer a range of sponsorship opportunities for industry (bronze, silver, gold and platinum), each with specific benefits. Please see the website for further details. -- 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/25b02a1a-6d41-4f51-9a73-e312054aab3a%40gmail.com.
Chalmers University of Technology in Gothenburg, Sweden is hiring up to five PhD students: https://www.chalmers.se/en/about-chalmers/work-with-us/vacancies/?rmpage=job&rmjob=12588&rmlang=UK One of the proposed projects, "A compiler for cubical type theory", is related to homotopy type theory. As a PhD student working on this project you would be supervised by me and part of a group which currently includes Andreas Abel, Robin Adams, Jean-Philippe Bernardy, Ana Bove, Thierry Coquand, Peter Dybjer, Ulf Norell and Christian Sattler, as well as postdocs and PhD students. Note that this kind of position comes with a salary and benefits, and that there are no tuition fees. Application deadline: April 15. -- /NAD -- 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/6bc4ac9e-352e-4a93-a6f4-46d790d336fe%40cse.gu.se.
COST Action CA20111 EuroProofNet Open call for Short-Term Scientific Missions (STSMs) and Inclusive Target Conference Grants (ITCGs) Dear Action members, The next deadline for STSM and ITCG proposals is: 17 March 2024 *What is an STSM?* A Short-Term Scientific Mission (STSM) is a research visit of an individual researcher from a country participating in the Action in a different country also participating in the Action. We encourage STSMs, as they are an effective way of starting and maintaining research collaborations. *What is an ITC conference grant?* ITC Conference Grants are given to young (<= 40 years old) researchers affiliated in an Inclusiveness Target Country or Near Neighbour Country to present a work related to EuroProofNet in a high-level conference fully organized by a third party, i.e. not organized nor co-organized by EuroProofNet. Reimbursement rules are the same as for STSMs. We especially welcome proposals from the working groups 4, and from inclusive-target countries and women. STSM and ITCG proposals should be between April and September 2024. Find all the details concerning application on https://europroofnet.github.io/grants/ Do not hesitate to contact us if you have any questions. Best wishes, Simona Prokić and Ambrus Kaposi EuroProofNet Grant Awarding Coordinators -- 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/87v86gvk1a.fsf%40neumann.mail-host-address-is-not-set.
[-- Attachment #1: Type: text/plain, Size: 3337 bytes --] ========================================================== REGISTRATION FOR Workshop on Homotopy Type Theory and Univalent Foundations (HoTT/UF 2024, co-located with WG6 meeting of the EuroProofNet COST action) ========================================================== ------------------------------------------------------------------------ Workshop on Homotopy Type Theory and Univalent Foundations April 2 - 3, 2024, Leuven, Belgium https://hott-uf.github.io/2024/ Co-located with the WG6 meeting of the EuroProofNet COST action April 4 - 5, 2024 https://europroofnet.github.io/wg6-leuven/ ------------------------------------------------------------------------ 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/Univalent Foundations: from the study of syntax and semantics of type theory to practical formalization in proof assistants based on univalent type theory. The workshop will be held in person with support for remote participation. We encourage online participation for those who do not wish to or cannot travel. ================ # Registration Please register by filling out this form: https://docs.google.com/forms/d/17WFBrTRoa9f3ZkKDpDlPAQFwvEFTreOAqbxC4XWLO14/ Registration is mandatory (also if you're attending online only). Registration deadline: March 8, 2024 ================ # Invited speakers * Mathieu Anel (Carnegie Mellon University, USA) * Rafaël Bocquet (Eötvös Loránd University, Hungary) * Matthias Hutzler (University of Gothenburg, Sweden) ================ # Contributed talks Authors and titles of contributed talks are listed on the website. ================ # Program committee * Pierre Cagne (Applachian State University) * Evan Cavallo (University of Gothenburg) * Felix Cherubini (Chalmers University of Technology/University of Gothenburg) * Tom de Jong (University of Nottingham) * Eric Finster (University of Birmingham) * Daniel Gratzer (Aarhus University) * Mitchell Riley (NYU Abu Dhabi) * Michael Shulman (University of San Diego) * Kristina Sojakova (INRIA Paris) * Jon Sterling (University of Cambridge) * Andrew Swan (University of Ljubljana) * Jonathan Weinberger (Johns Hopkins University) ================ # Organizers * Evan Cavallo, evan.cavallo@gu.se (University of Gothenburg) * Tom de Jong, tom.dejong@nottingham.ac.uk (University of Nottingham) * Mitchell Riley, mitchell.v.riley@nyu.edu (NYU Abu Dhabi) * Jonathan Weinberger, jweinb20@jhu.edu (Johns Hopkins University) -- 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/CAOOoPfUTFp8JWjj6qbA5isUA%3DKFKgUFeYHVSPi%2BUy9zEssc6CQ%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 4270 bytes --]
Hi y'all, I'd like to encourage those of you working on mathematical aspects of HoTT to submit your relevant work to the Canadian Journal of Mathematics (more than 20 pages) and the Canadian Mathematical Bulletin (at most 20 pages). https://www.cambridge.org/core/journals/canadian-journal-of-mathematics https://www.cambridge.org/core/journals/canadian-mathematical-bulletin It's good for our community to be visible in general math journals such as CJM and CMB, and now there is, shall we say, a sympathetic editor. Best, Chris -- 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/32263316-e226-4dc0-834f-601366f099e0%40gmail.com.
[-- Attachment #1.1: Type: text/plain, Size: 1714 bytes --] Dear all, If you are a student currently looking for a PhD position in the field of HoTT, please see the advert below. Additional information can be found at: https://www.cs.nott.ac.uk/~pszgmh/10-phds.html --------------------------------------------- ------------------------------------------------------- The School of Computer Science at the University of Nottingham in the UK is seeking applications for 10 fully-funded PhD studentships: http://tinyurl.com/ten-phd-2024 Applicants in the area of the Functional Programming Lab (tinyurl.com/fp-notts) are strongly encouraged! If you are interested in applying, please contact a potential supervisor as soon as possible; the application deadline is 7th April 2024: Thorsten Altenkirch - constructive logic, proof assistants, homotopy type theory, category theory, lambda calculus. Ulrik Buchholtz - homotopy type theory, synthetic homotopy theory, proof assistants, constructive mathematics, and related topics. Graham Hutton - not currently seeking a new student. Nicolai Kraus - homotopy type theory, higher category theory, constructive mathematics, and related topics. Dan Marsden - category theory, logic, finite model theory, diagrammatic reasoning, foundations of computer science. Best wishes, The FP Lab University of Nottingham -- 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/39c7198e-5e87-4119-a825-9d82ffe19a19n%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 6865 bytes --]
****************************************************************** *** PhD Position *** A Correct-by-Construction Approach to Approximate Computation *** Mathematically Structured Programming Group *** University of Strathclyde (Glasgow) ***************************************************************** Applications are invited for a fully funded UK PhD studentship in the areas of type theory, category theory and/or logic, under the supervision of Dr Fredrik Nordvall Forsberg, and Professors Neil Ghani and Radu Mardare. The research will be part of the recently EPSRC-funded project "A Correct-by-Construction Approach to Approximate Computation", which seeks to develop type-theoretic tools and frameworks for approximation. The position is for 3 years, with a start date of 1 October 2024. It includes both coverage of fees and an stipend, and is open to UK-based applicants. The successful applicant will become part of the Mathematically Structured Programming group (https://msp.cis.strath.ac.uk) at the University of Strathclyde. It is likely that you will also work with the other members in the group, which include Conor McBride, Robert Atkey, Glynn Winskel, Jules Hedges, Guillaume Allais, and currently 10 PhD students. We are located in the city centre of Glasgow, with plenty of both culture and nature nearby. Scotland is a great place for theoretical computer science: we have active collaborations with researchers Edinburgh, Heriot-Watt, Glasgow and St. Andrews. Applications, requests for further information, and other informal enquiries can be sent to: Fredrik Nordvall Forsberg fredrik.nordvall-forsberg@strath.ac.uk If you are interested, please get in touch as soon as you can. We hope to appoint in early March. Best wishes, Fred -- 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/81dd63d8-770e-4273-ad1e-e9fc675e483d%40strath.ac.uk.
https://www.cs.le.ac.uk/events/mgs2024/ The Midlands Graduate School (MGS) provides an intensive programme of lectures on the Mathematical Foundations of Computing Science. It has run annually since 1999 and has been held at either the University of Birmingham, the University of Leicester, the University of Nottingham, or at the University of Sheffield. The lectures are aimed at postgraduate/PhD students, typically in their first or second year of study for a PhD. However, the school is open to anyone who is interested in learning more about mathematical computing foundations, and all such applicants are warmly welcomed. We very much encourage students from abroad to attend, participants from industry, and many have done so in the past. Celebrating 25 Years, MGS 2024 will be held at the School of Computing and Mathematics, University of Leicester, U.K. -- 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/31b22711-e7da-49e0-9738-a2571912f71c%40gmail.com.
7th International Conference on Applied Category Theory (ACT) 40th Conference on Mathematical Foundations of Programming Semantics (MFPS) This year, the ACT and MFPS conferences will be co-located in Oxford. https://oxford24.github.io/ Conference dates: ACT 2024: 17 - 21 June 2024 MFPS 2024: 19 - 21 June 2024 Submission deadlines: ACT 2024: 29 March 2024 MFPS 2024: 29 March 2024 For details see: https://oxford24.github.io/act_cfp.html https://oxford24.github.io/mfps_cfp.html Programme Chairs: David Jaz Myers, Michael Johnson (ACT) Valeria de Paiva, Alex Simpson (MFPS) Local organization: Sam Staton (Oxford) and others -- 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/9E8B4859-9CD3-4E64-889D-AA6DD29D561D%40cs.ox.ac.uk.
[-- Attachment #1: Type: text/plain, Size: 1369 bytes --] We are advertising several PhD positions<https://jobs.nottingham.ac.uk/Vacancy.aspx?ref=SCI259> at Nottingham which includes the Functional Programming Laboratory. The group which includes Nicolai Kraus and Ulrik Buchholtz has got a strong interest in Type Theory in particular Homotopy Type Theory and its semantic foundations using (higher) category theory. We mainly use the agda system for formal developments. If you are interested, please contact me before applying. Cheers, Thorsten 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. -- 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/PAXPR06MB786905044BBBCC4FC0F71EEDCD4B2%40PAXPR06MB7869.eurprd06.prod.outlook.com. [-- Attachment #2: Type: text/html, Size: 3641 bytes --]
Logical Frameworks and Meta Languages: Theory and Practice (LFMTP24) https://lfmtp.github.io/lfmtp-page/workshops/2024/ ==================================================================== 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 2024 will provide researchers a forum to present state-of-the-art techniques and discuss progress in areas such as the following: * Design, Analysis, Implementation, Evaluation, and Application of logical frameworks like LF, Abella, Beluga, ELPI, Hybrid, lambdaPi, or MMT * Encoding and reasoning about the theory of programming languages, logical systems, type theories, and similar formal systems * Theoretical and practical issues concerning the treatment of variable binding such as higher-order abstract syntax, nominal logic, explicit substituations, or binding signatures * Representation and reasoning about features of logics and languages like equality, inductive and co-inductive definitions, inductive types of higher dimension, universes, as well as associated reasoning techniques * Frontiers of logical frameworks such as canonical and substructural frameworks, contextual frameworks, functional programming over logical frameworks, or homotopy and cubical type theory * Logical framework-based tools and services such as theorem proving, search tools, or IDEs * Two-level languages to program and reason over logics like tactic languages, reflection, or meta-programming in interactive provers such as LTac, ELPI, MetaCoq, Isabelle, and Lean's meta-programming), including implementation and use cases * Graphical languages for building proofs, applications in geometry, equational reasoning and category theory. ## Important Dates Abstract submission deadline: April 29 Paper submission deadline: May 6 Notification to authors: June 3 Final version due: June 13 Workshop: July 8 ## Submission and Proceedings We solicit regular papers of up to 15 pages (including references). These must be original and not simultaneously submitted to another venue. They will be reviewed, and we plan to publish (pre- or post-) proceedings in a series like EPTCS or similar. In addition, we encourage the submission of abstracts (1-4 pages including references) describing work-in-progress, new ideas, challenges, or other interesting informal contributions. All submitted papers should be in PDF format following the EPTCS style guidelines. Submissions should be made via easychair at https://easychair.org/conferences/?conf=lfmtp24. We will investigate the possibility of having a journal special issue for extended versions of selected contributions. ## Program Committee * Florian Rabe (University of Erlangen-Nuremberg), co-chair * Claudio Sacerdoti Coen (University of Bologna), co-chair * Mauricio Ayala-Rincón (University of Brasilia) * Mario Carneiro (Carnegie Mellon University) * Kaustuv Chaudhuri (École Polytechnique Paris) * Cyril Cohen (Inria Sophia Antipolis) * Theo Winterhalter (Inria Saclay) * Other members TBA -- Prof. Claudio Sacerdoti Coen Department of Computer Science and Engineering Coordinator of the Undergraduate and Graduate Programmes in Computer Science 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/5805637e8b03428ad79c1cd03d251f4cb41d16b6.camel%40unibo.it.
[-- Attachment #1: Type: text/plain, Size: 5323 bytes --] Call for Contributions TYPES 2024 30th International Conference on Types for Proofs and Programs Copenhagen, Denmark, 10 - 14 June 2024 https://types2024.itu.dk OVERVIEW -------- The TYPES meetings are a forum to present new and on-going work in all aspects of type theory and its applications, especially in formalised and computer assisted reasoning and computer programming. The TYPES areas of interest include, but are not limited to: * foundations of type theory and constructive mathematics; * applications of type theory; * dependently typed programming; * industrial uses of type theory technology; * meta-theoretic studies of type systems; * proof assistants and proof technology; * automation in computer-assisted reasoning; * links between type theory and functional programming; * formalizing mathematics using type theory. We encourage talks proposing new ways of applying type theory. In the spirit of workshops, talks may be based on newly published papers, work submitted for publication, but also work in progress. CONTRIBUTED TALKS ----------------- TYPES solicits contributed talks to stimulate discussions. Selection of those will be based on extended abstracts/short papers of 2 pp (not including bibliography) formatted with easychair.cls. IMPORTANT DATES --------------- * Submission of abstract 4 March 2024 AoE * Author notification 19 April 2024 AoE * Camera-ready version of abstract 10 May 2024 AoE * Conference 10 - 14 June 2024 Camera-ready versions of the accepted contributions will be published in an informal book of abstracts for distribution during the conference. POST-PROCEEDIGNS ---------------- A post-proceedings volume will be published in the Leibniz International Proceedings in Informatics (LIPIcs) series. Submission to that volume will be open to everyone. Tentative submission deadline for the post-proceedings: October 2024. PROGRAMME COMMITTEE ------------------- Patrick Bahr (IT University of Copenhagen, Denmark) (co-chair) Henning Basold (Leiden University, The Netherlands) Andrej Bauer (University of Ljubljana, Slovenia) Marco Carbone (IT University of Copenhagen, Denmark) Jesper Cockx (TU Delft, The Netherlands) Greta Coraglia (University of Milan, Italy) Peter Dybjer (Chalmers University of Technology, Sweden) Yannick Forster (INRIA, France) Hugo Herbelin (INRIA, France) Patricia Johann (Appalachian State University, USA) Marie Kerjean (CNRS, France) Ekaterina Komendantskaya (University of Southampton, United Kingdom) Meven Lennon-Bertrand (University of Cambridge, United Kingdom) Assia Mahboubi (INRIA, France) Sonia Marin (University of Birmingham, United Kingdom) Anders Mörtberg (Stockholm University, Sweden) Rasmus Ejlers Møgelberg (IT University of Copenhagen, Denmark) (co-chair) Benjamin Pierce (University of Pennsylvania, USA) Jakob Rehof (Technical University of Dortmund, Germany) Simona Ronchi Della Rocca (University of Turin, Italy) Kristina Sojakova (Vrije Universiteit Amsterdam, The Netherlands) Ana Sokolova (University of Salzburg, Austria) Bas Spitters (Aarhus University, Denmark) Wouter Swierstra (Utrecht University, The Netherlands) Philip Wadler (University of Edinburgh, United Kingdom) TYPES STEERING COMMITTEE ------------------------ Sandra Alves (University of Porto, Portugal) Eduardo Hermo Reyes (Formal Vindications, Spain) Rasmus Ejlers Møgelberg (IT University of Copenhagen, Denmark) Paige Randall North (Utrecht University, The Netherlands) (chair) Matthieu Sozeau (INRIA & Université de Nantes, France) Benno van den Berg (University of Amsterdam, The Netherlands) (secretary) ABOUT TYPES ----------- The TYPES meetings from 1990 to 2008 were annual workshops of a sequence of five EU funded networking projects. From 2009 to 2021, TYPES has been run as an independent conference series. Previous TYPES meetings were held in Antibes (1990), Edinburgh (1991), Båstad (1992), Nijmegen (1993), Båstad (1994), Torino (1995), Aussois (1996), Kloster Irsee (1998), Lökeberg (1999), Durham (2000), Berg en Dal near Nijmegen (2002), Torino (2003), Jouy-en-Josas near Paris (2004), Nottingham (2006), Cividale del Friuli (2007), Torino (2008), Aussois (2009), Warsaw (2010), Bergen (2011), Toulouse (2013), Paris (2014), Tallinn (2015), Novi Sad (2016), Budapest (2017), Braga (2018), Oslo (2019), Virtual (2021), Nantes (2022), València (2023). CONTACT ------- Email: types2024@easychair.org ORGANIZERS ---------- Patrick Bahr (IT University of Copenhagen, Denmark) Marco Carbone (IT University of Copenhagen, Denmark) Rasmus Ejlers Møgelberg (IT University of Copenhagen, Denmark) -- 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/CAO0VQQb0O%3DMhLN4ZVSo_Mb%3DBSb8CtrX39HVBqXwOU%2BPhddCGig%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 6111 bytes --]
[-- Attachment #1.1: Type: text/plain, Size: 7671 bytes --] CiE 2024: CALL FOR PAPERS Computability in Europe 2024 Twenty years of theoretical and practical synergies Amsterdam, The Netherlands July 08-12, 2024 https://events.illc.uva.nl/CiE/CiE2024/ Submission link: https://equinocs.springernature.com/service/CiE2024 IMPORTANT DATES: Deadline for article submission: February 10, 2024 (AOE) Notification of acceptance: April 20, 2024 Final versions due: May 1, 2024 Deadline for informal presentations submission: May 15, 2024 (The notifications of acceptance for informal presentations will be sent a few days after submission) Early registration before: May 20, 2024 Conference: July 08-12, 2024 GENERAL INFORMATION CiE 2024 will be an anniversary event. It is the 20th conference organized by CiE (Computability in Europe), in the same place as the first edition, Amsterdam. CiE is a European association of mathematicians, logicians, computer scientists, philosophers, physicists and others interested in new developments in computability and their underlying significance for the real world. Previous meetings have taken place in Amsterdam (2005), Swansea (2006), Siena (2007), Athens (2008), Heidelberg (2009), Ponta Delgada (2010), Sofia (2011), Cambridge (2012), Milan (2013), Budapest (2014), Bucharest (2015), Paris (2016), Turku (2017), Kiel (2018), Durham (2019), Salerno (2020, virtually), Ghent (2021, virtually), Swansea (2022) and Batumi (2023). TUTORIAL SPEAKERS Matthew Harrison-Trainor (University of Illinois Chicago) Sonja Smets (University of Amsterdam) INVITED SPEAKERS Arnold Beckmann (Swansea University) Rod Downey (Victoria University of Wellington) Elvira Mayordomo (University of Zaragoza) Alexandre Miquel (Universidad de la República) Monika Seisenberger (Swansea University) Mariya Soskova (University of Wisconsin–Madison) SPECIAL SESSIONS There will be 6 special sessions: - Computable aspects of symbolic dynamics and tilings (chairs: Benjamin Hellouin and Ilkka Torma) - Algorithmic randomness and Kolmogorov complexity session (chairs: Rupert Hölzl abd Denis Hirschfeldt) - Quantum Computation (chairs: Delaram Kahrobaei and Mehrnoosh Sadrzadeh) - History and Philosophy of Computing (HaPoC) (chairs: Ekaterina Koubychkina and Marianna Girlando) - Bio-inspired Computation (BiC) (chairs: Gianluca Della Vedova and Jasmijn Baaijens) - Computable Structure Theory (chairs: Stefan Vatev and Ekaterina Fokina) CONFERENCE TOPICS The CiE conferences serve as an interdisciplinary forum for research in all aspects of computability, foundations of computer science, logic, and theoretical computer science, as well as the interplay of these areas with practical issues in computer science and with other disciplines such as biology, mathematics, philosophy, or physics. PAPER SUBMISSION THE PROGRAM COMMITTEE cordially invites all researchers, European and non-European, to submit their papers in all areas related to the above for presentation at the conference. The following paper categories are welcome: - Regular papers describing solid new research results. Papers submitted to the conference proceedings should represent original work, not simultaneously submitted to another journal or conference with formal proceedings. The Program Committee will rigorously review and select submitted papers. Regular papers must have a maximum of 12 pages, including references but excluding a possible appendix in which one can include proofs and other additional material. Papers building bridges between different parts of the research community are particularly welcome. - Informal presentations. Continuing the tradition of past CiE conferences, we invite researchers to present informal presentations of their recent work. A proposal for an informal presentation must be 1 page long; a brief description of the results suffices and an abstract is not required. Informal presentations will not be published in the LNCS conference proceedings. Results presented as informal presentations at CiE 2024 may appear or may have appeared in other conferences with formal proceedings and/or in journals. All submissions must be in PDF, formatted using the Springer LNCS style (available at https://www.springer.com/gp/computer-science/lncs/conference-proceedings-guidelines), and submitted via EquinOCS: https://equinocs.springernature.com/service/CiE2024 CONFERENCE PROCEEDINGS Accepted regular papers will be published as a proceedings volume in the Lecture Notes in Computer Science (LNCS) series from Springer-Verlag. PROGRAM COMMITTEE Contributed papers will be selected from submissions received by the PROGRAM COMMITTEE consisting of: Bahareh Afshari (University of Amsterdam & University of Gothenburg) Nathalie Aubrun (CNRS, Université Paris-Saclay) Marie-Pierre Béal (Université Gustave Eiffel) Benno van den Berg (University of Amsterdam) Sebastian Berndt (University of Lübeck) Patricia Bouyer-Decitre (CNRS) Jin-Yi Cai (University of Wisconsin-Madison) Barbara Csima (University of Waterloo) Gianluca Della Vedova (Università degli Studi di Milano-Bicocca) Leah Epstein (University of Haifa) Gilda Ferreira (Universidade Aberta) Yannick Foster (INRIA, Nantes) Lorenzo Galeotti (Amsterdam University College) Mathieu Hoyrup (INRIA, LORIA, Nancy) Jarkko Kari (University of Turku) Julia Knight (University of Notre-Dame) Susana Ladra (Universidade da Coruña) Timo Lang (Technische Universität Wien) Karen Lange (Wellesley College) Florin Manea (University of Göttingen) Alexander Melnikov (Victoria University of Wellington) Alberto Naibo (Université Paris 1 Panthéon-Sorbonne) Ludovic Patey (CNRS, Université Paris-Cité co-Chair) Elaine Pimentel (University College London co-chair) Cristóbal Rojas (Universidad Católica) Viola Schiaffonati (Politecnico di Milano) Paul Shafer (University of Leeds) Reed Solomon (University of Connecticut) Andreas Weiermam (Ghent University) WOMEN IN COMPUTABILITY We are very happy to announce that within the framework of the Women in Computability program, we are able to offer some grants for junior women researchers who want to participate in CiE 2024. Applications for this grant should be sent to Lorenzo Galeotti <l.galeotti@uva.nl>, before May 15, 2024 and include a short cv (at most 2 pages) and contact information for an academic reference. Preference will be given to junior women researchers who are presenting a paper (including informal presentations) at CiE 2024. HOSTED BY The event will be held in the Amsterdam University College academic building located at Amsterdam Science Park. We are grateful for support from the University of Amsterdam and the Vrije Universiteit Amsterdam. ORGANIZING COMMITTEE Bahareh Afshari (University of Gothenburg) Luis Aguilar Suarez (Amsterdam University College) Benno van den Berg (University of Amsterdam) Andrea De Domenico (Vrije Universiteit Amsterdam) Tamara Dobler (Vrije Universiteit Amsterdam) Lorenzo Galeotti (Amsterdam University College -- chair) Yurii Khomskii (Amsterdam University College) Mattia Panettiere (Vrije Universiteit Amsterdam) Benjamin Rin (Universiteit Utrecht) -- 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/39b8f17f-6cc6-4c73-9454-12b439fe86d9n%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 8126 bytes --]
[-- Attachment #1: Type: text/plain, Size: 3564 bytes --] ========================================================== FINAL CALL FOR CONTRIBUTIONS AND PARTICIPATION Workshop on Homotopy Type Theory and Univalent Foundations (HoTT/UF 2024, co-located with WG6 meeting of the EuroProofNet COST action) ========================================================== ------------------------------------------------------------------------ Workshop on Homotopy Type Theory and Univalent Foundations April 2 - 3, 2024, Leuven, Belgium https://hott-uf.github.io/2024/ Co-located with the WG6 meeting of the EuroProofNet COST action April 4 - 5, 2024 https://europroofnet.github.io/wg6-leuven/ ------------------------------------------------------------------------ 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/Univalent Foundations: from the study of syntax and semantics of type theory to practical formalization in proof assistants based on univalent type theory. The workshop will be held in person with support for remote participation. We encourage online participation for those who do not wish to or cannot travel. ================ # Invited speakers * Rafaël Bocquet (Eötvös Loránd University, Hungary) * Matthias Hutzler (University of Gothenburg, Sweden) * TBA ================ # Submissions * Abstract submission deadline: January 19, 2024 * Author notification: Mid-February 2024 Submissions should consist of a title and a 1-2 pages abstract, in pdf format, via https://easychair.org/conferences/?conf=hottuf2024. Considering the broad background of the expected audience, we encourage authors to include information of pedagogical value in their abstract, such as motivation and context of their work. ================ # Registration Registration is mandatory with a deadline of 8 March 2024 (AoE). Registration information will be provided shortly. ================ # Program committee * Pierre Cagne (Applachian State University) * Evan Cavallo (University of Gothenburg) * Felix Cherubini (Chalmers University of Technology/University of Gothenburg) * Tom de Jong (University of Nottingham) * Eric Finster (University of Birmingham) * Daniel Gratzer (Aarhus University) * Mitchell Riley (NYU Abu Dhabi) * Michael Shulman (University of San Diego) * Kristina Sojakova (INRIA Paris) * Jon Sterling (University of Cambridge) * Andrew Swan (University of Ljubljana) * Jonathan Weinberger (Johns Hopkins University) ================ # Organizers * Evan Cavallo, evan.cavallo@gu.se (University of Gothenburg) * Tom de Jong, tom.dejong@nottingham.ac.uk (University of Nottingham) * Mitchell Riley, mitchell.v.riley@nyu.edu (NYU Abu Dhabi) * Jonathan Weinberger, jweinb20@jhu.edu (Johns Hopkins University) -- 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/CAOOoPfVsMQAZRLt2N08j8WoGLhWz7H%2Bw%3Dkbj3jYZ8D5z%2BfJucA%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 4464 bytes --]
As usual, we have openings for strong graduate applicants in all areas, and I in particular welcome applicants interested in homotopy type theory, homotopy theory and higher categories. Our department has lots of people working on these topics and many visitors and seminars. Note that the deadline of February 1 is coming soon, but that applications will continue to be reviewed after that. Our standard ad is below. Best, Dan ----- Please distribute to undergraduate and master's students and appropriate counsellors and supervisors. 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 a large number of fully funded positions available, and applicants from any country are welcome. Our faculty members supervise research in a variety of areas: https://www.math.uwo.ca/graduate/supervisors.html https://www.math.uwo.ca/research/ The Department of Mathematics is part of the School of Mathematical Sciences: https://uwo.ca/smss/ More information about our program, including the application procedure, is available at https://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/87bk9rd7og.fsf%40uwo.ca.
[-- Attachment #1: Type: text/plain, Size: 1243 bytes --] Dear colleagues and friends, [Apologies for multiple postings] This is a kind reminder of the deadline of 31st January 2024 for submissions of papers to the special issue of Mathematical Structures in Computer Science entitled “Advances in Homotopy Type Theory”. Submissions based on talks presented at the International Conference in Homotopy Type Theory held at Carnegie Mellon University in May 2023 are encouraged, but other papers are welcome too. Submissions should be made via the MSCS Scholar One portal, choosing the name of the special issue from the drop down list on page one: https://www.cambridge.org/core/journals/mathematical-structures-in-computer-science With best wishes of a happy 2024, Nicola (also on behalf of the other guest editors, Thorsten Altenkirch, Benno van den Berg, and Maria Emilia Maietti) -- 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/BA34FEB5-F152-4E73-BCA6-B7623DE50B71%40manchester.ac.uk. [-- Attachment #2: Type: text/html, Size: 1989 bytes --]
[-- Attachment #1.1: Type: text/plain, Size: 10338 bytes --] I stumbled upon this thread a (quite bit) late, so sorry for chiming in out of the blue. But I have a way of showing that EH(x,x) gets you a generator of pi3(S2) in HoTT. I a gave a short talk about it at CMU's HoTT2023, and should soon be submitting a revised write up to the special issue in MSCS. Its quite cool to see the construction of the expected generator of pi7(S4). It makes me wonder how much one could adapt what goes on in the EH and Hopf proof for these higher dimensions. Related, I think all thats missing from Noah's message that is required to compute pi4(S3) is a non-triviality proof. Is there a good reference for this in book HoTT? On Monday, July 10, 2023 at 12:49:33 PM UTC-6 Noah Snyder wrote: > For general p and q you need to assume that they're 4-loops, but if p=q > then it should hold for 3-loops! Analogously xx = xx for 1-loops, but xy = > yx only for 2-loops. Best, > > Noah > > On Mon, Jul 10, 2023 at 2:46 PM Kristina Sojakova <sojakova...@gmail.com> > wrote: > >> Thanks for all this Noah! Not being an expert, I will need some time to >> digest all the details, but my first question is this: I proved the >> equality of (4) and (5) for 4-loops p, q. Do we expect this should hold at >> a lower dimension too? >> On 7/10/2023 7:43 PM, Noah Snyder wrote: >> >> Very nice! I really like this line of research! >> >> Let me try my hand at sketching what consequences I think this has for >> homotopy groups of spheres. This isn't exactly my area of expertise so I >> may have messed up something here. There's a TL;DR below. >> >> As a warmup let's talk about Eckmann-Hilton itself. EH says that if x and >> y are 2-loops, then xy = yx. Since this involves two variables this is a >> statement about a homotopy group of a wedge of spheres S^2 wedge S^2, >> namely it says that the commutator xyx^-1y^-1 which is non-trivial in >> \pi_1(S^1 wedge S^1) becomes trivial when you suspend it to get an element >> of \pi_2(S^2 wedge S^2). In other words, it gives a new relation >> (commutativity) in \pi_2(S^2 wedge S^2). From this viewpoint we can also >> easily get a statements about homotopy groups of wedges of spheres for more >> elaborate constructions. In particular, the syllepsis says that a certain >> element of \pi_3(S^2 wedge S^2) vanishes when you suspend it to \pi_4(S^3 >> wedge S^3). Finally, the "syllepsis of the syllepsis" (henceforth SoS, >> though see the postscript) says that a certain element of pi_5(S^3 wedge >> S^3) vanishes when you suspend it to pi_6(S^4 wedge S^4). >> >> Ok, but people are usually more interested in homotopy groups of spheres, >> rather than of wedges of two spheres. So let's go back to Eckmann-Hilton >> and think some more. We can consider EH where both variables are the same >> loop x (or, if you prefer, one is x and the other is x^-1) so that now >> we're talking about homotopy groups of a single sphere. Here something >> interesting happens, note that EH now gives an equality xx = xx, but we >> already knew xx = xx! Indeed if you look at the suspension map \pi_1(S^1) >> --> \pi_2 (S^2) it's an isomorphism, so we're not adding a new relation. >> Instead we're saying that xx = xx in two different ways! First xx = xx via >> refl but second xx = xx via EH. If we compose one of these trivializations >> with the inverse of the other, what we end up with is a new element of >> pi_3(S^2). This is how EH is related to pi_3(S^2). >> >> Now let's think about what the syllepsis says about homotopy groups of >> spheres. So now we again want to look at the syllepsis of x with itself. >> This tells us that the element of pi_3(S^2) that we constructed from EH >> composed with itself will become trivial when suspended into pi_4(S^3). In >> this case this is killing 2 in Z, and so it really does add a new relation. >> >> Ok, now let's turn to SoS, and again restrict our attention to SoS of x >> with itself. This says that a certain element of pi_5(S^3) vanishes when >> suspended to pi_6(S^4). But if you look at the homotopy groups the map >> pi_5(S^3) --> pi_6(S^4) is already an isomorphism (this is analogous to >> what happened for EH!), in particular the paths (4) and (5) from Kristina's >> paper are already equal when p = q without assuming they're 4-loops! (I >> haven't thought at all how one would go about proving this though!) So >> instead we do what we did for EH, for a 4-loop x we have two different ways >> of showing (4) = (5) and this gives us an interesting element of pi_7(S^4). >> And looking in the table there is an interesting new element of pi_7(S^4) >> that doesn't come from pi_6(S^3), and I'd guess this construction gives >> this new generator of pi_7(S^4). >> >> Remark: Note that in general there's not a 1-to-1 relationship between >> interesting generators and relations in the homotopy groups of spheres >> (which are operations of one variable!) and interesting operations of two >> variables. You might need to write down a pretty elaborate composition of >> operators in two variables to write down a generator or relation in >> homotopy groups of spheres. In particular, the generator of pi_4(S^2) is a >> more elaborate composition (it's essentially EH applied to EH), the >> relation 2=0 in pi_4(S^2) is also more elaborate, and the generator of >> pi_6(S^3) is much much more elaborate! (In particular, the generator of >> pi_6(S^3) was essentially constructed by Andre Henriques, but in globular >> instead of HoTT so it's missing all the unitors and associators. Even >> without all the associators and unitors it's already extremely complicated! >> See http://globular.science/1702.001v2) >> >> TL;DR: First show that if you assume p = q then (4) = (5) is already true >> for 3-loops. Then taking p to be a 4-loop compose the proof of (4) = (5) >> using that p=q with the inverse of the syllepsis of the syllepsis and >> you'll get an element of pi_7(S^4) which hopefully is the generator of the >> copy of Z in Z x Z/12 = pi_7(S^4). >> >> Best, >> >> Noah >> >> p.s. I wanted to push back a little on this "syllepsis of the syllepsis" >> name. The "syllepsis" gets its name because it's what you need to turn a >> "braided monoidal 2-category" into a "sylleptic monoidal 2-category." >> (Sylleptic in turn is just "symmetric" but changing "m" to "l" to make it a >> little bit less symmetric.) The "syllepsis of the syllepsis" by contrast is >> what's needed to turn a "sylleptic monoidal 2-category" into a "symmetric >> monoidal 2-category." That is, the parallel name would be the "symmetsis" >> or something similar. Perhaps a better nomenclature would be to use the E1 >> = monoidal, E2 = braided monoidal, E3, etc. phrasing which isn't specific >> to 2-categories. So you might call Eckman-Hilton the E2-axiom, the >> syllepsis the E3-axiom, and the SoS the E4-axiom. There will also be an >> E5-axiom, though because of stability you won't see that when studying >> 2-categories, it'll come up when you look at 3-categories. Another way you >> might talk about it is the syllepsis is the "coherence of EH" while the >> syllepsis of the syllepsis is "the coherence of the coherence of EH" which >> I think maybe matches how you're thinking about the word sylleptsis? >> >> On Sat, Jul 8, 2023 at 4:14 PM Kristina Sojakova <sojakova...@gmail.com> >> wrote: >> >>> Hello David, >>> On 7/8/2023 4:00 PM, David Roberts wrote: >>> >>> Dear Kristina, >>> >>> Am I correct in assuming that the "syllepsis for syllepsis" is the >>> equality of (4) and (5) in your paper? >>> >>> Indeed, we show the equality between (4) and (5). >>> >>> >>> Is this related to the fact stable pi_2 is Z/2? >>> >>> We do not yet understand the implications of this result, that's another >>> interesting question I guess. Do you have a conjecture here? >>> >>> Kristina >>> >>> >>> Best, >>> >>> On Sat, 8 July 2023, 10:46 pm Kristina Sojakova, <sojakova...@gmail.com> >>> wrote: >>> >>>> Dear Andrej, >>>> >>>> Indeed, my message could have been more user-friendly. The file >>>> contains >>>> alternative proofs of Eckmann-Hilton and syllepsis, together with the >>>> proofs of the coherences described in Section 8 of >>>> >>>> https://inria.hal.science/hal-03917004v1/file/syllepsis.pdf >>>> >>>> The last coherence outlined in the paper is what I referred to as >>>> "syllepsis for syllepsis". >>>> >>>> Best, >>>> >>>> Kristina >>>> >>>> On 7/8/2023 2:22 PM, andrej...@andrej.com wrote: >>>> > Dear Kristina, >>>> > >>>> > any chance you could spare a few words in English on the content of >>>> your formalization? Not everyone reads Coq code for breakfast. >>>> > >>>> > Many thanks in advance! >>>> > >>>> > Andrej >>>> > >>>> >>>> -- >>>> 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 HomotopyTypeThe...@googlegroups.com. >>>> To view this discussion on the web visit >>>> https://groups.google.com/d/msgid/HomotopyTypeTheory/8e549102-49ca-407f-e95f-22d971f4b9fe%40gmail.com >>>> . >>>> >>> -- >>> 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 HomotopyTypeThe...@googlegroups.com. >>> To view this discussion on the web visit >>> https://groups.google.com/d/msgid/HomotopyTypeTheory/7a08f997-1433-177d-ab99-b45ea4a14a8f%40gmail.com >>> <https://groups.google.com/d/msgid/HomotopyTypeTheory/7a08f997-1433-177d-ab99-b45ea4a14a8f%40gmail.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/44399e68-2981-4ff6-8787-4da7c347b2c4n%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 16049 bytes --]
SECOND CALL FOR PAPERS Thirty-Ninth Annual ACM/IEEE Symposium on LOGIC IN COMPUTER SCIENCE (LICS) Tallinn, July 2024 https://lics.siglog.org/lics24 SCOPE The LICS Symposium is an annual international forum on theoretical and practical topics in computer science that relate to logic, broadly construed. We invite submissions on topics that fit under that rubric. Suggested, but not exclusive, topics of interest include: automata theory, automated deduction, categorical models and logics, concurrency and distributed computation, constraint programming, constructive mathematics, database theory, decision procedures, description logics, domain theory, finite model theory, formal aspects of program analysis, formal methods, foundations of computability, foundations of probabilistic, real-time and hybrid systems, games and logic, higher-order logic, knowledge representation and reasoning, lambda and combinatory calculi, linear logic, logic programming, logical aspects of AI, logical aspects of bioinformatics, logical aspects of computational complexity, logical aspects of quantum computation, logical frameworks, logics of programs, modal and temporal logics, model checking, process calculi, programming language semantics, proof theory, reasoning about security and privacy, rewriting, type systems, type theory, and verification. IMPORTANT DATES FOR PAPERS Authors are required to submit a paper title and a short abstract of about 100 words in advance of submitting the extended abstract of the paper. The exact deadline time on these dates is anywhere on earth (AoE). Titles and Short Abstracts Due: 21 January 2024 Full Papers Due: 26 January 2024 Author Feedback/Rebuttal Period: 18-23 March 2024 Author Notification: 15 April 2024 Conference: 8-12 July 2024. Submission deadlines are firm; late submissions will not be considered. All submissions will be electronic via easychair. PAPER SUBMISSION INSTRUCTIONS Submissions should use ACM SIGCONF Proceedings 2-column 10pt format and may be at most 12 pages, excluding references. Latex style files and further submission information is at https://lics.siglog.org/lics24/cfp.php. LICS 2024 will use a lightweight double-blind reviewing process. Please see the website for further details and requirements from the double-blind process. The official publication date may differ from the first day of the conference. The official publication date may affect the deadline for any patent filings related to published work. We will clarify the official publication date in due course. -- 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/97F4CAE4-8490-4AE8-AA1B-E00BBE81F099%40cs.ox.ac.uk.
7th International Conference on Applied Category Theory (ACT 2024) 40th Conference on Mathematical Foundations of Programming Semantics (MFPS) 17 - 21 June 2024 Oxford, UK https://oxford24.github.io/ Preceeded by the Adjoint School 10 - 14 June 2024 https://adjointschool.com/ Conference submission deadline 29 March 2024. (Adjoint School application deadline 31 December 2023.) Programme Chairs: David Jaz Myers, Michael Johnson (ACT) Valeria de Paiva, Alex Simpson (MFPS) Local organization: Sam Staton (Oxford) and others -- 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/97BA9429-44E1-4E3E-8157-C2F4B1473F19%40cs.ox.ac.uk.
[-- Attachment #1: Type: text/plain, Size: 3558 bytes --] ========================================================== 2ND CALL FOR CONTRIBUTIONS AND PARTICIPATION Workshop on Homotopy Type Theory and Univalent Foundations (HoTT/UF 2024, co-located with WG6 meeting of the EuroProofNet COST action) ========================================================== ------------------------------------------------------------------------ Workshop on Homotopy Type Theory and Univalent Foundations April 2 - 3, 2024, Leuven, Belgium https://hott-uf.github.io/2024/ Co-located with the WG6 meeting of the EuroProofNet COST action April 4 - 5, 2024 https://europroofnet.github.io/wg6-leuven/ ------------------------------------------------------------------------ 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/Univalent Foundations: from the study of syntax and semantics of type theory to practical formalization in proof assistants based on univalent type theory. The workshop will be held in person with support for remote participation. We encourage online participation for those who do not wish to or cannot travel. ================ # Invited speakers * Rafaël Bocquet (Eötvös Loránd University, Hungary) * Matthias Hutzler (University of Gothenburg, Sweden) * TBA ================ # Submissions * Abstract submission deadline: January 19, 2024 * Author notification: Mid-February 2024 Submissions should consist of a title and a 1-2 pages abstract, in pdf format, via https://easychair.org/conferences/?conf=hottuf2024. Considering the broad background of the expected audience, we encourage authors to include information of pedagogical value in their abstract, such as motivation and context of their work. ================ # Registration Registration is mandatory with a deadline of 8 March 2024 (AoE). Registration information will be provided shortly. ================ # Program committee * Pierre Cagne (Applachian State University) * Evan Cavallo (University of Gothenburg) * Felix Cherubini (Chalmers University of Technology/University of Gothenburg) * Tom de Jong (University of Nottingham) * Eric Finster (University of Birmingham) * Daniel Gratzer (Aarhus University) * Mitchell Riley (NYU Abu Dhabi) * Michael Shulman (University of San Diego) * Kristina Sojakova (INRIA Paris) * Jon Sterling (University of Cambridge) * Andrew Swan (University of Ljubljana) * Jonathan Weinberger (Johns Hopkins University) ================ # Organizers * Evan Cavallo, evan.cavallo@gu.se (University of Gothenburg) * Tom de Jong, tom.dejong@nottingham.ac.uk (University of Nottingham) * Mitchell Riley, mitchell.v.riley@nyu.edu (NYU Abu Dhabi) * Jonathan Weinberger, jweinb20@jhu.edu (Johns Hopkins University) -- 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/CAOOoPfWAgye44iHW_zR-a_oX%2B4yc6UKxFYSF1kdSqmmAK_xHSQ%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 4454 bytes --]
Applications for the 2024 CMU Summer School in Logic and Formal Epistemology are now officially open! https://www.cmu.edu/dietrich/philosophy/undergraduate/summer-school/ June 3–7 Francesca Zaffora Blando & Krzysztof Mierzewski "Chance and Randomness” June 10–14 Jonas Frey & Reid Barton "Categorical Semantics and Synthetic Topology” June 17–21 Clark Glymour & Kun Zhang "The Logic of Discovery” The school runs for 3 weeks, June 3–21, and is open to all undergraduate and early-stage graduate students. There is no tuition and on-campus lodging is provided free of charge for the duration of the program. Applications close February 14. Any questions can be sent to abjorn@cmu.edu. -- 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/92FFCBD2-D171-4B16-B99D-0CDA6E3B65BE%40andrew.cmu.edu.