[TYPES/announce] Postdoctoral fellowship at Stockholm University
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Interested in doing a postdoc on logic and related topics in Stockholm? Applications are open for Sverker Lerheden postdoctoral fellowships in the Department of Mathematics at Stockholm University: https://urldefense.com/v3/__https://www.su.se/department-of-mathematics/news/sverker-lerheden-fellowships-for-postdoctoral-studies-1.682597__;!!IBzWLUs!TihImC59578Z4KvO1l2nZ3DsHs0n2u5aLofonSV21ttH9TPtUzqRXV2_E4lS55ihxs6htQnMj-DX9UY7puvf4wiKagCFz_zRjJIhEhk$ Application deadline: *November 16* Please contact me and Peter LeFanu Lumsdaine if you have any questions or are interested in applying as you will need a letter of support from us. Junior candidates will be given priority, so late stage and recently graduated PhD students are especially encouraged to apply. -- Anders
[TYPES/announce] Final call for participation (Deadline Friday 13 May): Workshop on Syntax and Semantics of Type Theories in Stockholm, Sweden, May 20-21, 2022
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] As previously announced, we are organizing an in-person workshop on Syntax and Semantics of Type Theories in Stockholm, Sweden, May 20-21, 2022. Details can be found at: https://urldefense.com/v3/__https://europroofnet.github.io/wg6-kickoff-stockholm/__;!!IBzWLUs!RzvbAQwLyd8l_4lxEk8SWgyTqE08SZtnBZ88IB7DmLdxRhfGsQ7GkFSybMnXNgJ-tIfP7opmYXv_b0XJvYH5GvskPcepOKutvLjljRY$ Registration is free, but required for planning purposes, by *Friday 13 May*. To register please fill out the form linked to on the event webpage. # Invited speakers: - Andrej Bauer - Anja Petković Komel - András Kovacs - Ivan Di Liberti - Jonathan Sterling - Taichi Uemura - Théo Winterhalter There will also be multiple contributed talks, for details see the schedule: https://urldefense.com/v3/__https://europroofnet.github.io/wg6-kickoff-stockholm/programme__;!!IBzWLUs!RzvbAQwLyd8l_4lxEk8SWgyTqE08SZtnBZ88IB7DmLdxRhfGsQ7GkFSybMnXNgJ-tIfP7opmYXv_b0XJvYH5GvskPcepOKutRcfpO00$ # Organisers * Benedikt Ahrens (TU Delft & University of Birmingham) * Peter LeFanu Lumsdaine (Stockholm University) * Anders Mörtberg (Stockholm University)
[TYPES/announce] Reminder: Workshop on Syntax and Semantics of Type Theories in Stockholm, Sweden, May 20-21 (contributed talk and funding deadline Monday 11 April)
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Reminder: the deadline to contribute a talk and applying for funding to participate in the workshop on type theory here in Stockholm is *Monday next week (11 April)*. For details see the email below. The meeting is open to anyone interested in type theory and the program will consist primarily of short talks, with plenty of time for discussions to share recent results, and co-ordinate future research. Everyone is very welcome to apply for funding regardless of whether one is contributing a talk or not. Priority will then be given to speakers, participants from “Inclusiveness Target Countries”, early-career researchers, and women (following the EU COST inclusiveness policy, details here <https://urldefense.com/v3/__https://www.cost.eu/about/cost-strategy/excellence-and-inclusiveness/__;!!IBzWLUs!COIgzJXLn4eOcvtnmpH5Sq0RZksu0_Yqbr78KvPPwz79F3QQtmZKyQhuOZetgXOgiFY0neYsVymNnw$ >). Best, Anders On Sun, Mar 27, 2022 at 6:27 PM Anders Mortberg wrote: > We are organizing a workshop on Syntax and Semantics of Type Theories in > Stockholm, Sweden, on May 20-21, 2022: > > https://urldefense.com/v3/__https://europroofnet.github.io/wg6-kickoff-stockholm/__;!!IBzWLUs!COIgzJXLn4eOcvtnmpH5Sq0RZksu0_Yqbr78KvPPwz79F3QQtmZKyQhuOZetgXOgiFY0neb2ht-NwQ$ > > > The event is intended as a kick-off meeting for working group 6 on type > theory of the EuroProofNet EU Cost Action: > > https://urldefense.com/v3/__https://europroofnet.github.io/wg6/__;!!IBzWLUs!COIgzJXLn4eOcvtnmpH5Sq0RZksu0_Yqbr78KvPPwz79F3QQtmZKyQhuOZetgXOgiFY0neY9WU9W1A$ > > > The programme will consist primarily of short talks, with plenty of time > for discussion to share recent results, and co-ordinate future research, > including collaboration towards deliverables. On the Sunday after the > workshop, there will be an informal social excursion — details TBA. The > meeting will be in-person. > # Confirmed speakers (more TBA) > > * András Kovacs > * Andrej Bauer > * Anja Petkovic Komel > * Ivan Di Liberti > * Jonathan Sterling > * Taichi Uemura > * Théo Winterhalter > > # Deadlines > > Contributed talks deadline: *Monday 11 April* > Funding request deadline: *Monday 11 April* > Participation registration deadline: *Friday 13 May* > > To register please fill out the form linked to on the event webpage. > > # Organisers > > * Benedikt Ahrens (TU Delft & University of Birmingham) > * Peter LeFanu Lumsdaine (Stockholm University) > * Anders Mörtberg (Stockholm University) > >
[TYPES/announce] Workshop on Syntax and Semantics of Type Theories in Stockholm, Sweden, on May 20-21, 2022
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] We are organizing a workshop on Syntax and Semantics of Type Theories in Stockholm, Sweden, on May 20-21, 2022: https://urldefense.com/v3/__https://europroofnet.github.io/wg6-kickoff-stockholm/__;!!IBzWLUs!F1vFHyLfRbA2OYww3lxoDeJpcyxydQvAaAsUuFgus5H7NqzQ3-F7p2HRE2KuHO8QNDCsbX4NictioA$ The event is intended as a kick-off meeting for working group 6 on type theory of the EuroProofNet EU Cost Action: https://urldefense.com/v3/__https://europroofnet.github.io/wg6/__;!!IBzWLUs!F1vFHyLfRbA2OYww3lxoDeJpcyxydQvAaAsUuFgus5H7NqzQ3-F7p2HRE2KuHO8QNDCsbX4H7EK8Cw$ The programme will consist primarily of short talks, with plenty of time for discussion to share recent results, and co-ordinate future research, including collaboration towards deliverables. On the Sunday after the workshop, there will be an informal social excursion — details TBA. The meeting will be in-person. # Confirmed speakers (more TBA) * András Kovacs * Andrej Bauer * Anja Petkovic Komel * Ivan Di Liberti * Jonathan Sterling * Taichi Uemura * Théo Winterhalter # Deadlines Contributed talks deadline: *Monday 11 April* Funding request deadline: *Monday 11 April* Participation registration deadline: *Friday 13 May* To register please fill out the form linked to on the event webpage. # Organisers * Benedikt Ahrens (TU Delft & University of Birmingham) * Peter LeFanu Lumsdaine (Stockholm University) * Anders Mörtberg (Stockholm University)
[TYPES/announce] Reminder: 2 year position on HoTT and related topics in Stockholm, deadline Friday next week
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Dear all, A quick reminder of the postdoctoral position in HoTT and related topics that I advertised a couple of weeks ago, with deadline *October 1* (midnight Stockholm time). Full details and application at: https://urldefense.com/v3/__https://www.su.se/english/about-the-university/work-at-su/available-jobs?rmpage=job&rmjob=15797&rmlang=UK__;!!IBzWLUs!DtuZsNTodN62rcs7_yEB1aKIn1Xx8dTk9UiLbqd1uYMpxjvbcYqcbVS_QBUW8oYrJdHrxn_2FSOquA$ Departmental webpage: https://urldefense.com/v3/__https://www.math.su.se/english/research__;!!IBzWLUs!DtuZsNTodN62rcs7_yEB1aKIn1Xx8dTk9UiLbqd1uYMpxjvbcYqcbVS_QBUW8oYrJdHrxn-xPny4KA$ Once again, please get in touch with me if you have any questions about the position or application process! Best, Anders On Mon, Sep 6, 2021 at 1:43 PM Anders Mortberg wrote: > Dear all, > > I’m pleased to announce that we’re hiring a postdoctoral researcher in > homotopy type theory and related topics at Stockholm University. It’s a 2 > year position, provisionally starting January 2022, in the computational > mathematics group of the Mathematics Department. The application deadline > is 1 October. > > We welcome all applicants interested in working on homotopy type theory > and related topics. Potential project topics include, but are not limited > to: homotopy type theory, categorical models of type theories, cubical type > theories, implementation of proof assistants, computer formalization of > mathematics and computer science. > > Full details and application at: > https://urldefense.com/v3/__https://www.su.se/english/about-the-university/work-at-su/available-jobs?rmpage=job&rmjob=15797&rmlang=UK__;!!IBzWLUs!DtuZsNTodN62rcs7_yEB1aKIn1Xx8dTk9UiLbqd1uYMpxjvbcYqcbVS_QBUW8oYrJdHrxn_2FSOquA$ > > > Departmental webpage: > https://urldefense.com/v3/__https://www.math.su.se/english/research__;!!IBzWLUs!DtuZsNTodN62rcs7_yEB1aKIn1Xx8dTk9UiLbqd1uYMpxjvbcYqcbVS_QBUW8oYrJdHrxn-xPny4KA$ > > > Please get in touch with me if you have any questions about the position! > > Best, > Anders > >
[TYPES/announce] Postdoctoral position in homotopy type theory and related topics at Stockholm University
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Dear all, I’m pleased to announce that we’re hiring a postdoctoral researcher in homotopy type theory and related topics at Stockholm University. It’s a 2 year position, provisionally starting January 2022, in the computational mathematics group of the Mathematics Department. The application deadline is 1 October. We welcome all applicants interested in working on homotopy type theory and related topics. Potential project topics include, but are not limited to: homotopy type theory, categorical models of type theories, cubical type theories, implementation of proof assistants, computer formalization of mathematics and computer science. Full details and application at: https://urldefense.com/v3/__https://www.su.se/english/about-the-university/work-at-su/available-jobs?rmpage=job&rmjob=15797&rmlang=UK__;!!IBzWLUs!HW4ucEENQqx0BeLkozigKEQZvUCYDHotG1kK5qIwWKsCeLbO6op2tU3PfHYbudVh0FwcIjXC5tgMKw$ Departmental webpage: https://urldefense.com/v3/__https://www.math.su.se/english/research__;!!IBzWLUs!HW4ucEENQqx0BeLkozigKEQZvUCYDHotG1kK5qIwWKsCeLbO6op2tU3PfHYbudVh0FwcIjUx0D4ePg$ Please get in touch with me if you have any questions about the position! Best, Anders
[TYPES/announce] PhD positions in Computational Mathematics at Stockholm University
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] The Department of Mathematics at Stockholm University invites applications for PhD positions in Computational Mathematics. A prospective student will have the opportunity to engage in exciting research related to type theory, HoTT/UF, constructive mathematics, programming language theory and category theoretic foundations. The student will be part of the newly founded Computational Mathematics division. It will also be possible to collaborate with other groups in the department, such as the Mathematical Logic group (with experts on constructive mathematics and type theory like Per Martin-Löf and Peter LeFanu Lumsdaine) and the Algebra, Geometry, Topology, and Combinatorics group. For further information and instructions on how to apply see https://www.su.se/english/about/working-at-su/phd?rmpage=job&rmjob=11944&rmlang=UK The deadline for application is April 23, 2020. Some potential project ideas can be found at https://www.math.su.se/english/education/phd-studies/research-projects/possible-research-projects-in-computational-mathematics-1.430102#m%C3%B6rtberg If you are interested in applying and have any questions feel free to contact me! -- Anders Mörtberg https://staff.math.su.se/anders.mortberg/
[TYPES/announce] Second CFP - Mathematical Logic and Constructivity (MLoC) 2019 : The Scope and Limits of Neutral
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] = Second Call for Participation and Contributed Papers = Mathematical Logic and Constructivity: The Scope and Limits of Neutral Constructivism Stockholm, Sweden, August 20-23, 2019 http://logic.math.su.se/mloc-2019/ Deadline for contributed talks: May 31, 2019 = With Errett Bishop's seminal work Foundations of Constructive Analysis 1967, a neutral position in the foundations of constructive mathematics emerged. It avoided Brouwer's assumptions about choice-sequences and continuity, and it did not assume that every total function on the natural numbers is computable. This made the position palatable also to the classical mathematician, and it is in the intersection of the three realms of foundations, commonly designated by the abbreviations INT, RUSS and CLASS. Successful full-fledged formal logical foundations for neutral constructivism exists, among the most well-known are Aczel-Myhill set theory and Martin-Löf type theory. Neutral constructive mathematics may also be studied for systems that make fewer ontological assumptions, which is important for reverse mathematics. To the surprise of many in constructive mathematics a new principle about sequences, the boundedness principle BD-N, was discovered, and found to be true in all the three realms without being true in neutral constructvism. Further principles of this kind are being investigated. In type theory new axioms have been discovered, such as the univalence axiom, whose constructive status was only later settled. Important questions are whether new axioms can be modelled indirectly using neutral constructive methods, or whether they can be directly justified. This workshop aims to focus on the scope and limits of neutral constructivism. The study of neutral constructivism paves the way for further developments of interactive proof systems, which is of strategic importance for verification of software, and in particular, correctness-by-construction software. INVITED SPEAKERS INCLUDE * Douglas S. Bridges, University of Canterbury, Christchurch, New Zealand * Thierry Coquand, Chalmers and Göteborg University, Sweden * Martin Escardo, University of Birminham, England (to be confirmed) * Makoto Fujiwara, Meiji University Tokyo, Japan * Nicola Gambino, Leeds University, England * Henri Lombardi, Université Franche-Comté, France * Maria Emilia Maietti, University of Padova, Italy * Takako Nemoto, JAIST, Japan * Iosif Petrakis, L-M University, Munich, Germany * Hideki Tsuiki, Kyoto University, Japan (to be confirmed) * Chuangjie Xu, L-M University, Munich, Germany * Keita Yokoyama, JAIST, Japan FURTHER SPEAKERS * Hajime Ishihara, JAIST, Japan * Anders Mörtberg, Carnegie Mellon University and Stockholm University CONTRIBUTED TALKS Proposals for contributed talks are welcome and are to be submitted via the EasyChair system: https://easychair.org/conferences/?conf=mloc19 Suggested length of abstract: half a page. Deadline for contributed talks: May 31, 2019 (anywhere on Earth) Notification of acceptance: June 14, 2019 PROGRAM COMMITTEE * Hajime Ishihara, JAIST, Japan (co-chair) * Tatsuji Kawai, JAIST, Japan * Peter LeFanu Lumsdaine, Stockholm University * Anders Mörtberg, Carnegie Mellon University and Stockholm University * Erik Palmgren, Stockholm University (co-chair) REGISTRATION The workshop is free of charge, but to aid planning please register by sending the organizers an email mlo...@math.su.se with name and affilliation at the latest August 13, 2019. TRAVEL GRANTS A limited number of travel and accommodation grants are available for contributed speakers and/or younger participants. Please write to mlo...@math.su.se if you are interested in applying for these. VENUE Department of Mathematics, Stockholm University, Sweden WEB PAGES http://logic.math.su.se/mloc-2019/ IMPORTANT DATES 2 April 2019 registration opens 31 May 2019 abstracts for contributed talks 14 June 2019 notification of acceptance 13 August 2019 registration closes 20-23 August 2019 conference
[TYPES/announce] PhD position in Computational Mathematics at Stockholm University
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] The Department of Mathematics at Stockholm University invites applications for a PhD position in Computational Mathematics. A prospective student will have the opportunity to engage in exciting research related to programming logic, type theory, constructive mathematics and category theoretic foundations. The student will be part of the newly founded Computational Mathematics division. It will also be possible to collaborate with other groups in the department, such as the Mathematical Logic group (with experts on constructive mathematics and type theory like Per Martin-Löf, Erik Palmgren and Peter LeFanu Lumsdaine) and the Algebra, Geometry, Topology, and Combinatorics group. For further information and instructions on how to apply see https://www.su.se/english/about/working-at-su/phd?rmpage=job&rmjob=8652&rmlang=UK The deadline for application is April 23, 2019. If you are interested in applying and have any questions feel free to contact me. -- Anders Mörtberg
[TYPES/announce] Final Call for Contributions: Workshop on Homotopy Type Theory and Univalent Foundations (HoTT/UF'18)
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] == FINAL CALL FOR CONTRIBUTIONS Workshop on Homotopy Type Theory and Univalent Foundations (HoTT/UF, at FLoC 2018) == NEWS: 1 week left until submission deadline! (April 15) NEWS: FLoC provides travel stipends for student attendees of FLoC’18 with application deadline May 18. For details see: http://www.floc2018.org/travel-stipend/ 4th Workshop on Homotopy Type Theory and Univalent Foundations July 7-8, 2018, Oxford, United Kingdom https://hott-uf.github.io/2018 Co-located with FSCD 2018 and part of FLoC 2018 http://www.cs.le.ac.uk/events/fscd2018/ http://www.floc2018.org/ Abstract submission deadline: April 15 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. == # Invited talks * Martín Escardó (University of Birmingham) * Paige North (Ohio State University) * Andrew Pitts (University of Cambridge) # Submissions * Abstract submission deadline: April 15 * Author notification: end of April Submissions should consist of a title and a 1-2 pages abstract, in pdf format, via https://easychair.org/conferences/?conf=hottuf18 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. == # Program committee * Benedikt Ahrens (University of Birmingham) * Paolo Capriotti (University of Nottingham) * Simon Huber (University of Gothenburg) * Chris Kapulkin (University of Western Ontario) * Nicolai Kraus (University of Nottingham) * Peter LeFanu Lumsdaine (Stockholm University) * Assia Mahboubi (Inria Saclay) * Anders Mörtberg (Carnegie Mellon University and University of Gothenburg) * Nicolas Tabareau (Inria Nantes) # Organizers * Benedikt Ahrens (University of Birmingham) * Simon Huber (University of Gothenburg) * Anders Mörtberg (Carnegie Mellon University and University of Gothenburg)
[TYPES/announce] Call for Contributions: Workshop on Homotopy Type Theory and Univalent Foundations (HoTT/UF'18)
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] == 2nd CALL FOR CONTRIBUTIONS Workshop on Homotopy Type Theory and Univalent Foundations (HoTT/UF, at FLoC 2018) == NEWS: submission deadline changed to April 15 (was March 31) to align with general submission deadline of FLoC workshops. Workshop on Homotopy Type Theory and Univalent Foundations July 7-8, 2018, Oxford, United Kingdom https://hott-uf.github.io/2018 Co-located with FSCD 2018 and part of FLoC 2018 http://www.cs.le.ac.uk/events/fscd2018/ http://www.floc2018.org/ Abstract submission deadline: April 15 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. == # Invited talks * Martín Escardó (University of Birmingham) * Paige North (Ohio State University) * Andrew Pitts (University of Cambridge) # Submissions * Abstract submission deadline: April 15 * Author notification: end of April Submissions should consist of a title and a 1-2 pages abstract, in pdf format, via https://easychair.org/conferences/?conf=hottuf18 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. == # Program committee * Benedikt Ahrens (University of Birmingham) * Paolo Capriotti (University of Nottingham) * Simon Huber (University of Gothenburg) * Chris Kapulkin (University of Western Ontario) * Nicolai Kraus (University of Nottingham) * Peter LeFanu Lumsdaine (Stockholm University) * Assia Mahboubi (Inria Saclay) * Anders Mörtberg (Carnegie Mellon University and University of Gothenburg) * Nicolas Tabareau (Inria Nantes) # Organizers * Benedikt Ahrens (University of Birmingham) * Simon Huber (University of Gothenburg) * Anders Mörtberg (Carnegie Mellon University and University of Gothenburg)
[TYPES/announce] Call for Contributions: Workshop on Homotopy Type Theory and Univalent Foundations (HoTT/UF'18)
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] == CALL FOR CONTRIBUTIONS Workshop on Homotopy Type Theory and Univalent Foundations (HoTT/UF, at FLoC 2018) == Workshop on Homotopy Type Theory and Univalent Foundations July 7-8, 2018, Oxford, United Kingdom https://hott-uf.github.io/2018 Co-located with FSCD 2018 and part of FLoC 2018 http://www.cs.le.ac.uk/events/fscd2018/ http://www.floc2018.org/ Abstract submission deadline: March 31 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. == # Invited talks * Martín Escardó (University of Birmingham) * Paige North (Ohio State University) * Andrew Pitts (University of Cambridge) # Submissions * Abstract submission deadline: March 31 * Author notification: mid April Submissions should consist of a title and a 1-2 pages abstract, in pdf format, via https://easychair.org/conferences/?conf=hottuf18 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. == # Program committee * Benedikt Ahrens (University of Birmingham) * Paolo Capriotti (University of Nottingham) * Simon Huber (University of Gothenburg) * Chris Kapulkin (University of Western Ontario) * Nicolai Kraus (University of Nottingham) * Peter LeFanu Lumsdaine (Stockholm University) * Assia Mahboubi (Inria Saclay) * Anders Mörtberg (Carnegie Mellon University and University of Gothenburg) * Nicolas Tabareau (Inria Nantes) # Organizers * Benedikt Ahrens (University of Birmingham) * Simon Huber (University of Gothenburg) * Anders Mörtberg (Carnegie Mellon University and University of Gothenburg)
[TYPES/announce] Open call for papers: Special Issue on Homotopy Type Theory and Univalent Foundations
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Open call for papers for a Special Issue of Mathematical Structures in Computer Science in association with the workshops on Homotopy Type Theory and Univalent Foundations HoTT/UF 2017-2018 https://hott-uf.github.io/special-issue-17-18/ BACKGROUND Homotopy Type Theory is a young research area 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 and higher category theory. Univalent Foundations are foundations of mathematics based on the homotopical interpretation of type theory. These ideas have led to many interesting developments, from the study of syntax and semantics of type theories to practical formalizations in proof assistants based on univalent type theory. The HoTT/UF workshops, co-located with FSCD since 2016, started out as a forum for formalization of mathematics in a univalent setting. From the 2017 edition and onwards, its scope has been broadened to encompass all aspects of Homotopy Type Theory and Univalent Foundations, in particular (but not exclusively): - semantics of (univalent) type theory, - computational content of the univalence axiom, - syntax and semantics of higher inductive types, - synthetic homotopy theory, and - formalization of mathematics and computer science in Homotopy Type Theory and Univalent Foundations. SPECIAL ISSUE We are soliciting submissions for a Special Issue of the journal *Mathematical Structures in Computer Science* (Cambridge University Press) edited in association with the 2017 and 2018 editions of the HoTT/UF workshop. Submission is open to everyone and not limited to workshop participants. Submission is open from now and contributions will be reviewed on a *rolling basis*, as soon as they are received. Accepted papers will be published on the MSCS website via 'FirstView' and will be citeable through a DOI shortly after acceptance - before the completion of the whole journal issue (expected end of 2019). Submission will be closed on December 31, 2018. For details and submission instructions see: https://hott-uf.github.io/special-issue-17-18/ GUEST EDITORS * Benedikt Ahrens * Simon Huber * Anders Mörtberg
[TYPES/announce] Call for Participation: Workshop on HoTT/UF (with FSCD 2017)
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] == CALL FOR PARTICIPATION Workshop on Homotopy Type Theory and Univalent Foundations (HoTT/UF, at FSCD 2017) September 8-9, 2017, Oxford, United Kingdom https://hott-uf.github.io/2017/ == Contents: 1. Invited talks 2. Contributed talks now on the website 3. Post-proceedings with MSCS 1. Invited talks/tutorials == * Thorsten Altenkirch (University of Nottingham): Naïve Type Theory (tutorial) * Ulrik Buchholtz (Technical University of Darmstadt): Formalizing type theory in type theory using nominal techniques * Thierry Coquand (University of Gothenburg): Sheaf models for univalent type theory 2. Contributed talks Titles and abstracts for the contributed talks are now available on the website: https://hott-uf.github.io/2017/ 3. Post-proceedings with MSCS = The publication of post-proceedings of the HoTT/UF'17 workshop is being planned, as a special issue of *Mathematical Structures in Computer Science* (CUP). Submission to the post-proceedings will be open to all, with a submission deadline in late spring 2018. More details will be announced in due course.
[TYPES/announce] 2nd Call for Contributions and Participation: Workshop on HoTT/UF (with FSCD 2017)
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] == CALL FOR CONTRIBUTIONS AND PARTICIPATION Workshop on Homotopy Type Theory and Univalent Foundations (HoTT/UF, at FSCD 2017) == Workshop on Homotopy Type Theory and Univalent Foundations September 8-9, 2017, Oxford, United Kingdom https://hott-uf.github.io/2017/ Co-located with FSCD 2017 https://www.cs.ox.ac.uk/conferences/fscd2017/ Abstract submission deadline: June 30 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. As part of the workshop there will be an introductory tutorial intended to make the invited and contributed talks accessible to non-experts. # Invited talks/tutorials * Thorsten Altenkirch (University of Nottingham) (tutorial) * Ulrik Buchholtz (Technical University of Darmstadt) * Thierry Coquand (University of Gothenburg): Sheaf models for univalent type theory # Submissions * Abstract submission deadline: June 30 * Author notification: mid July Submissions should consist of a title and a 1-2 pages abstract, in pdf format, via https://easychair.org/conferences/?conf=hottuf17 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. == # Program committee * Benedikt Ahrens (Inria Nantes) * Paolo Capriotti (University of Nottingham) * Simon Huber (University of Gothenburg) * Chris Kapulkin (University of Western Ontario) * Peter LeFanu Lumsdaine (Stockholm University) * Assia Mahboubi (Inria Saclay) * Anders Mörtberg (Inria Sophia-Antipolis) * Paige North (University of Cambridge) * Nicolas Tabareau (Inria Nantes) # Organizers * Benedikt Ahrens (Inria Nantes) * Simon Huber (University of Gothenburg) * Anders Mörtberg (Inria Sophia Antipolis)
