From andrei.h.popescu at gmail.com Mon Jan 8 12:00:00 2024 From: andrei.h.popescu at gmail.com (Andrei Popescu) Date: Mon, 8 Jan 2024 11:00:00 +0000 Subject: [Agda] LMS/BCS-FACS online talk by Lawrence Paulson, 15 January 2024 Message-ID: Dear all, Next week there will be an online talk (via zoom) by Lawrence Paulson on a topic that is likely to be of interest to quite a few people on these lists. Please note the information about registration below. Best wishes, Andrei Information: https://www.bcs.org/events-calendar/2024/january/webinar-formalising-21st-century-mathematics/ Date/Time: 15 January 2024, 4-6pm GMT Speaker: Lawrence C. Paulson FRS, University of Cambridge Web: https://www.cl.cam.ac.uk/~lp15/ Registration: https://www.lms.ac.uk/events/lms-bcs-facs-seminar-2024 Title: Formalising 21st-Century Mathematics Abstract: The formalisation of mathematics is an ongoing process that arguably started as early as the 19th century, intensified with the foundational crisis at the start of the 20th century, and since the 1970s has been conducted with the help of computers. Recent decades have seen the machine formalisation of lengthy and technically complicated proofs, but some have argued that even these were not representative of modern mathematics. Recent achievements by a number of different groups are starting to challenge this scepticism. The speaker will outline some of these, while also noting some of the remaining trouble spots. Biography: Lawrence Paulson FRS is an American computer scientist. He is a Professor of Computational Logic at the University of Cambridge Computer Laboratory and a Fellow of Clare College, Cambridge. He is best known for the cornerstone text on the programming language ML, ML for the Working Programmer. His research is based around the interactive theorem prover Isabelle, which he introduced in 1986. He has worked on the verification of cryptographic protocols using inductive definitions, and he has also formalised the constructible universe of Kurt G?del. Recently he has built a new theorem prover, MetiTarski, for real-valued special functions. From andrei.h.popescu at gmail.com Mon Jan 8 13:46:44 2024 From: andrei.h.popescu at gmail.com (Andrei Popescu) Date: Mon, 8 Jan 2024 12:46:44 +0000 Subject: [Agda] LMS/BCS-FACS online talk by Lawrence Paulson, 15 January 2024 In-Reply-To: References: Message-ID: Dear colleagues, Another note: This talk will be recorded and made available on youtube (I will come back with the link). I would like to apologise to those of you attending CPP -- when scheduling this (which happened a while ago) I lost sight of the overlap with CPP. :-( Best wishes, Andrei On Mon, Jan 8, 2024 at 11:00?AM Andrei Popescu wrote: > > Dear all, > > Next week there will be an online talk (via zoom) by Lawrence Paulson > on a topic that is likely to be of interest to quite a few people on > these lists. Please note the information about registration below. > > Best wishes, > Andrei > > Information: https://www.bcs.org/events-calendar/2024/january/webinar-formalising-21st-century-mathematics/ > > Date/Time: 15 January 2024, 4-6pm GMT > Speaker: Lawrence C. Paulson FRS, University of Cambridge > Web: https://www.cl.cam.ac.uk/~lp15/ > > Registration: https://www.lms.ac.uk/events/lms-bcs-facs-seminar-2024 > > Title: Formalising 21st-Century Mathematics > > Abstract: The formalisation of mathematics is an ongoing process that > arguably started as early as the 19th century, intensified with the > foundational crisis at the start of the 20th century, and since the > 1970s has been conducted with the help of computers. Recent decades > have seen the machine formalisation of lengthy and technically > complicated proofs, but some have argued that even these were not > representative of modern mathematics. Recent achievements by a number > of different groups are starting to challenge this scepticism. The > speaker will outline some of these, while also noting some of the > remaining trouble spots. > > Biography: Lawrence Paulson FRS is an American computer scientist. He > is a Professor of Computational Logic at the University of Cambridge > Computer Laboratory and a Fellow of Clare College, Cambridge. He is > best known for the cornerstone text on the programming language ML, ML > for the Working Programmer. His research is based around the > interactive theorem prover Isabelle, which he introduced in 1986. He > has worked on the verification of cryptographic protocols using > inductive definitions, and he has also formalised the constructible > universe of Kurt G?del. Recently he has built a new theorem prover, > MetiTarski, for real-valued special functions. From tdejong.ac at gmail.com Fri Jan 12 10:38:20 2024 From: tdejong.ac at gmail.com (Tom de Jong) Date: Fri, 12 Jan 2024 09:38:20 +0000 Subject: [Agda] HoTT/UF 2024: Final Call for Contributions (Deadline: 19 Jan 2024) Message-ID: <5030b7e1-216d-4861-9026-cd2b0f31420e@gmail.com> ========================================================== 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 at gu.se (University of Gothenburg) * Tom de Jong, tom.dejong at nottingham.ac.uk (University of Nottingham) * Mitchell Riley, mitchell.v.riley at nyu.edu (NYU Abu Dhabi) * Jonathan Weinberger, jweinb20 at jhu.edu (Johns Hopkins University) From Graham.Hutton at nottingham.ac.uk Mon Jan 15 09:32:47 2024 From: Graham.Hutton at nottingham.ac.uk (Graham Hutton) Date: Mon, 15 Jan 2024 08:32:47 +0000 Subject: [Agda] Fully-funded PhD studentship in functional programming Message-ID: Dear all, I'm advertising a fully-funded PhD studentship in functional programming, starting 1st October 2024. Please pass the advert on to anyone who may be intersted in applying. Best wishes, Graham Hutton +-----------------------------------------------------------+ Fully-Funded PhD Studentship Functional Programming Lab School of Computer Science University of Nottingham, UK http://tinyurl.com/fplab-phd Applications are invited for a fully-funded PhD studentship under the supervision of Prof Graham Hutton, starting on 1st October 2024. The successful applicant will join the Functional Programming Lab, an internationally-leading centre for programming language research. The topic for the studentship is open, but should relate to the research interests of Prof Hutton on the mathematics of program construction. The studentship forms part of the recently-funded EPSRC project on Semantics-Directed Compiler Construction, which seeks to develop new techniques for constructing certified compilers from semantics. The studentship is open to home and international students, is fully-funded for three and a half years, and includes a stipend of ?18,622 per year and tuition fees. Applicants are expected to have a first-class Masters or Bachelors degree (or equivalent) in Computer Science and/or Mathematics, and an excellent ability and interest in the mathematical foundations of programming, together with experience of programming in a functional language. Further information and advice for prospective applicants is available from http://tinyurl.com/369xwzc7. Funding for this studentship is already in place. To apply, please submit the following items by email to graham.hutton at nottingham.ac.uk: (1) a brief covering letter that describes your reasons for wishing to undertake a PhD and any ideas you have about potential topics; (2) a copy of your CV, including your actual or expected degree class(es) and results of all university examinations; (3) an example of your technical writing, such as a report or dissertation; (4) email addresses for two academic referees. Closing date for applications: Friday 9th February 2024. +-----------------------------------------------------------+ ? Professor Graham Hutton School of Computer Science University of Nottingham, UK http://www.cs.nott.ac.uk/~pszgmh This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law. From Graham.Hutton at nottingham.ac.uk Fri Feb 2 08:01:33 2024 From: Graham.Hutton at nottingham.ac.uk (Graham Hutton) Date: Fri, 2 Feb 2024 07:01:33 +0000 Subject: [Agda] PhD studentship in functional programming (closing date 9th Feb) Message-ID: Dear all, If you are interested in applying for the advertised PhD studentship in functional programming, please note that the closing date is now one week away (9th February). Best wishes, Graham +-----------------------------------------------------------+ Fully-Funded PhD Studentship Functional Programming Lab School of Computer Science University of Nottingham, UK http://tinyurl.com/fplab-phd Applications are invited for a fully-funded PhD studentship under the supervision of Prof Graham Hutton, starting on 1st October 2024. The successful applicant will join the Functional Programming Lab, an internationally-leading centre for programming language research. The topic for the studentship is open, but should relate to the research interests of Prof Hutton on the mathematics of program construction. The studentship forms part of the recently-funded EPSRC project on Semantics-Directed Compiler Construction, which seeks to develop new techniques for constructing certified compilers from semantics. The studentship is open to home and international students, is fully-funded for three and a half years, and includes a stipend of ?18,622 per year and tuition fees. Applicants are expected to have a first-class Masters or Bachelors degree (or equivalent) in Computer Science and/or Mathematics, and an excellent ability and interest in the mathematical foundations of programming (topics such as logic and semantics), together with experience of programming in a functional language. Further information and advice for prospective applicants is available from http://tinyurl.com/369xwzc7. Funding for this studentship is already in place. To apply, please submit the following items by email to graham.hutton at nottingham.ac.uk: (1) a brief covering letter that describes your reasons for wishing to undertake a PhD and any ideas you have about potential topics; (2) a copy of your CV, including your actual or expected degree class(es) and results of all university examinations; (3) an example of your technical writing, such as a report or dissertation; (4) email addresses for two academic referees. Closing date for applications: Friday 9th February 2024. +-----------------------------------------------------------+ -- Professor Graham Hutton School of Computer Science University of Nottingham, UK http://www.cs.nott.ac.uk/~pszgmh This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law. From acie at acie.eu Wed Feb 7 16:53:32 2024 From: acie at acie.eu (acie at acie.eu) Date: Wed, 07 Feb 2024 16:53:32 +0100 Subject: [Agda] CiE 2024: CALL FOR PAPERS [Deadline Extension] Message-ID: <2e338629b5c959031ad44becec3fbf35@acie.eu> CiE 2024: CALL FOR PAPERS [Deadline Extension] 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 24, 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 , 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) -------------- next part -------------- An HTML attachment was scrubbed... URL: From claudio.sacerdoticoen at unibo.it Thu Feb 8 23:21:20 2024 From: claudio.sacerdoticoen at unibo.it (Claudio Sacerdoti Coen) Date: Thu, 8 Feb 2024 22:21:20 +0000 Subject: [Agda] CfP: Logica Frameworks and Meta Languages: Theory and Practice (LFMTP24) Message-ID: <5805637e8b03428ad79c1cd03d251f4cb41d16b6.camel@unibo.it> 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 From danel.ahman at ut.ee Fri Feb 9 06:01:28 2024 From: danel.ahman at ut.ee (Danel Ahman) Date: Fri, 9 Feb 2024 05:01:28 +0000 Subject: [Agda] Research Fellow in Programming Languages Foundations, University of Tartu, Estonia Message-ID: <5B24EB42-B163-475E-8C4F-56B0B7DF568F@ut.ee> The Institute of Computer Science at the University of Tartu invites applications for a Research Fellow position in Programming Languages. This is a permanent full-time position. The application deadline is 01.03.2024. We seek a strong candidate with demonstrated expertise in the foundations of programming languages. The successful candidate will work as part of the Laboratory for Software Science under the Chair of Programming Languages and Systems. Please consult our webpages to get an overview of our work: https://plas.cs.ut.ee For further details and requirements concerning the position, and for application instructions, see https://ut.ee/en/job-offer/research-fellow-programming-languages The knowledge of Estonian language is not a prerequisite for this position, but please note that international academic staff will have to reach at least a B1 level of Estonian language proficiency after five years of work in Estonia. Tartu is a pleasant student town easily reached from Tallinn, the capital of Estonia. It is one of the European Capitals of Culture in 2024. The University is one of the oldest in Northern Europe (est 1632), ranked #301-350 in the THE rankings 2024. The Institute of Computer Science is strong in a wide range of research areas, and has excellent modern premises and infrastructure. For any enquiries about the advertised position, you can contact me (danel.ahman at ut.ee) and Vesal Vojdani (vesal.vojdani at ut.ee). -------------- next part -------------- An HTML attachment was scrubbed... URL: From Thorsten.Altenkirch at nottingham.ac.uk Fri Feb 9 17:08:55 2024 From: Thorsten.Altenkirch at nottingham.ac.uk (Thorsten Altenkirch) Date: Fri, 9 Feb 2024 16:08:55 +0000 Subject: [Agda] PhD positions at Nottingham Message-ID: We are advertising several PhD positions 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. -------------- next part -------------- An HTML attachment was scrubbed... URL: From abela at chalmers.se Sun Feb 11 14:51:02 2024 From: abela at chalmers.se (Andreas Abel) Date: Sun, 11 Feb 2024 14:51:02 +0100 Subject: [Agda] [ANNOUNCE] Agda 2.6.4.2 release candidate In-Reply-To: References: Message-ID: Dear all, The Agda Team is pleased to announce a release candidate for Agda 2.6.4.2. Agda 2.6.4.2 is a bugfix release over Agda 2.6.4.1: - Fix an inconsistency in Cubical Agda related to catch-all clauses. - Fix some internal errors. - Fix an issue with `opaque`. - Fix building with cabal flag `-f debug-serialisation`. # GHC supported versions Agda 2.6.4.2 RC has been tested with GHC 9.8.1, GHC 9.6.4, 9.4.8, 9.2.8, 9.0.2, 8.10.7, 8.8.4 and 8.6.5 on Linux, macOS and Windows. # Installation Agda 2.6.4.2 RC can be installed using cabal-install or stack: 1. Getting the release candidate $ cabal get https://hackage.haskell.org/package/Agda-2.6.4.2/candidate/Agda-2.6.4.2.tar.gz $ cd Agda-2.6.4.2 2. a. Using cabal-install $ cabal install -f +optimise-heavily -f +enable-cluster-counting 2. b. Using stack $ stack --stack-yaml stack-a.b.c.yaml install --flag Agda:optimise-heavily --flag Agda:enable-cluster-counting replacing `a.b.c` with your version of GHC. The flags mean: - optimise-heavily: Turn on extra optimisation for a faster Agda. Takes large resources during compilation of Agda. - enable-cluster-counting: Enable unicode clusters for alignment in the LaTeX backend. Requires the ICU lib to be installed and known to pkg-config. These flags can be dropped from the install if causing trouble. # Standard library You can use standard library v1.7.3, v2.0 or the `master` branch of the standard library with Agda 2.6.4.2. This branch is available at https://github.com/agda/agda-stdlib/ # Fixed issues over Agda 2.6.4.1 https://hackage.haskell.org/package/Agda-2.6.4.2/candidate/changelog Enjoy the Agda 2.6.4.2 RC and please test as much as possible. Report problems and regressions to: https://github.com/agda/agda/issues Andreas, on behalf of the Agda Team -- Andreas Abel <>< Du bist der geliebte Mensch. Department of Computer Science and Engineering Chalmers and Gothenburg University, Sweden andreas.abel at gu.se http://www.cse.chalmers.se/~abela/ From m.escardo at bham.ac.uk Mon Feb 12 12:39:38 2024 From: m.escardo at bham.ac.uk (Martin Escardo) Date: Mon, 12 Feb 2024 11:39:38 +0000 Subject: [Agda] MGS'2024 (Midlands Graduate School) Message-ID: <8d91e1e0-12ad-4aef-9e87-955d8c5f7e30@bham.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. From fredrik.nordvall-forsberg at strath.ac.uk Tue Feb 13 18:32:30 2024 From: fredrik.nordvall-forsberg at strath.ac.uk (Fredrik Nordvall Forsberg) Date: Tue, 13 Feb 2024 17:32:30 +0000 Subject: [Agda] PhD position at the University of Strathclyde Message-ID: <81dd63d8-770e-4273-ad1e-e9fc675e483d@strath.ac.uk> ****************************************************************** *** 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 at 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 From bove at chalmers.se Thu Feb 15 17:23:14 2024 From: bove at chalmers.se (Ana Bove) Date: Thu, 15 Feb 2024 17:23:14 +0100 Subject: [Agda] Assistant professor positions in Computer science and engineering at Chalmers Message-ID: <4a1ddcaf-f69d-4872-bd0f-10e75182b2bc@chalmers.se> Dear All, The Department of Computer Science and Engineering , a join department between Chalmers and University of Gothenburg, has several job openings with calls open until mid March: up to two in cybersecurity, one across all of ICT, and one in ?basic science?, which typically means theoretical computer science. While two of the ads are very broad (that in ICT and basic science), CSE current focus is on the cybersecurity and AI/ML areas, _interpreted fairly broadly_; so candidates on these areas are particularly welcome on those calls. Some of these positions come with a generous package, for further details please look at the linked here: /Assistant Professor Positions in Cybersecurity/ https://www.chalmers.se/en/about-chalmers/work-with-us/vacancies/?rmpage=job&rmjob=12550&rmlang=UK /Assistant Professor in Information and Communication Technology: For a smarter and safer society/ https://www.chalmers.se/en/about-chalmers/work-with-us/vacancies/?rmpage=job&rmjob=12541&rmlang=UK /Assistant Professor in Basic Science: Pushing the boundaries of knowledge/ https://www.chalmers.se/en/about-chalmers/work-with-us/vacancies/?rmpage=job&rmjob=12538&rmlang=UK /_Applicants may apply for more than one of these position!_/ (the positions will be evaluated separately) Please do not hesitate to contact us if you have any questions. Yours sincerely -- -- Ana Bove, Docent Phone: (46)(31) 772 1020 http://www.cse.chalmers.se/~bove Department of Computer Science and Engineering Chalmers Univ. of Technology and Univ. of Gothenburg -------------- next part -------------- An HTML attachment was scrubbed... URL: From nicolai.kraus at gmail.com Fri Feb 16 19:20:49 2024 From: nicolai.kraus at gmail.com (Nicolai Kraus) Date: Fri, 16 Feb 2024 18:20:49 +0000 Subject: [Agda] PhD positions at Nottingham In-Reply-To: References: Message-ID: Below is the full advert for PhD studentships at Nottingham. If you are interested, please also see the information at https://www.cs.nott.ac.uk/~pszgmh/10-phds.html Cheers, Nicolai +-----------------------------------------------------------+ Dear all, 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 On Fri, Feb 9, 2024 at 4:09?PM Thorsten Altenkirch < Thorsten.Altenkirch at nottingham.ac.uk> wrote: > We are advertising several PhD positions > 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. > _______________________________________________ > Agda mailing list > Agda at lists.chalmers.se > https://lists.chalmers.se/mailman/listinfo/agda > -------------- next part -------------- An HTML attachment was scrubbed... URL: From abela at chalmers.se Sat Feb 17 12:38:09 2024 From: abela at chalmers.se (Andreas Abel) Date: Sat, 17 Feb 2024 12:38:09 +0100 Subject: [Agda] [ANNOUNCE] Agda 2.6.4.2 release candidate 2 In-Reply-To: References: Message-ID: <0b1cf18b-ffd9-4a9f-97bf-fa4df8d454f4@chalmers.se> Dear all, The Agda Team is pleased to announce a second release candidate for Agda 2.6.4.2. Changes over Agda 2.6.4.2 RC 1 are three more fixes: - [Issue #7104](https://github.com/agda/agda/issues/7104): Warning "there are two interface files" should not be serialized - [Issue #7105](https://github.com/agda/agda/issues/7105): Internal error in generate-helper (C-c C-h) - [Issue #7113](https://github.com/agda/agda/issues/7113): Instance resolution runs too late, leads to `with`-abstraction failure # GHC supported versions Agda 2.6.4.2 RC 2 has been tested with GHC 9.8.1, GHC 9.6.4, 9.4.8, 9.2.8, 9.0.2, 8.10.7, 8.8.4 and 8.6.5 on Linux, macOS and Windows. # Installation Agda 2.6.4.2 RC 2 can be installed using cabal-install or stack: 1. Getting the release candidate $ cabal get https://hackage.haskell.org/package/Agda-2.6.4.2/candidate/Agda-2.6.4.2.tar.gz $ cd Agda-2.6.4.2 2. a. Using cabal-install $ cabal install -f +optimise-heavily -f +enable-cluster-counting 2. b. Using stack $ stack --stack-yaml stack-a.b.c.yaml install --flag Agda:optimise-heavily --flag Agda:enable-cluster-counting replacing `a.b.c` with your version of GHC. The flags mean: - optimise-heavily: Turn on extra optimisation for a faster Agda. Takes large resources during compilation of Agda. - enable-cluster-counting: Enable unicode clusters for alignment in the LaTeX backend. Requires the ICU lib to be installed and known to pkg-config. These flags can be dropped from the install if causing trouble. # Standard library You can use standard library v1.7.3, v2.0 or the `master` branch of the standard library with Agda 2.6.4.2. This branch is available at https://github.com/agda/agda-stdlib/ # Fixed issues over Agda 2.6.4.1 https://hackage.haskell.org/package/Agda-2.6.4.2/candidate/changelog Enjoy the Agda 2.6.4.2 RC 2 and please test as much as possible. Report problems and regressions to: https://github.com/agda/agda/issues Andreas, on behalf of the Agda Team -- Andreas Abel <>< Du bist der geliebte Mensch. Department of Computer Science and Engineering Chalmers and Gothenburg University, Sweden andreas.abel at gu.se http://www.cse.chalmers.se/~abela/ _______________________________________________ Agda mailing list Agda at lists.chalmers.se https://lists.chalmers.se/mailman/listinfo/agda From tdejong.ac at gmail.com Mon Feb 19 12:05:44 2024 From: tdejong.ac at gmail.com (Tom de Jong) Date: Mon, 19 Feb 2024 11:05:44 +0000 Subject: [Agda] HoTT/UF 2024: Registration Message-ID: <86556ae0-1430-4342-8e3d-f870c6bf5ab1@gmail.com> ========================================================== 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 at gu.se (University of Gothenburg) * Tom de Jong, tom.dejong at nottingham.ac.uk (University of Nottingham) * Mitchell Riley, mitchell.v.riley at nyu.edu (NYU Abu Dhabi) * Jonathan Weinberger, jweinb20 at jhu.edu (Johns Hopkins University) From kaposi.ambrus at gmail.com Thu Feb 22 12:02:41 2024 From: kaposi.ambrus at gmail.com (Ambrus Kaposi) Date: Thu, 22 Feb 2024 12:02:41 +0100 Subject: [Agda] Call for STSMs and ITC conference grants, deadline 17 March 2024 Message-ID: <87v86gvk1a.fsf@neumann.mail-host-address-is-not-set> 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 From bove at chalmers.se Thu Feb 22 17:37:28 2024 From: bove at chalmers.se (Ana Bove) Date: Thu, 22 Feb 2024 17:37:28 +0100 Subject: [Agda] Five PhD Positions at the department of Computer Science and Engineering, Chalmers Message-ID: The department of Computer Science and Engineering at Chalmers has a broad call for up to *five fully funded PhD positions* in a variety of areas, among them *formal methods and type theory*. As a PhD student in Sweden you have a competitive monthly salary and full social benefits (paid sick and parental leave, pension benefits, etc). PhD program is designed for 5 years and includes 20% of departmental duties, which in general means helping as a teaching assistants in courses offered at the department. For more information, including the list of projects potential candidates can apply to, please have a look at the following link https://www.chalmers.se/en/about-chalmers/work-with-us/vacancies/?rmpage=job&rmjob=12588&rmlang=UK _Deadline for application is April 15th 2024._ Do not hesitate to contact us if you have any questions regarding the call or the projects! -- -- Ana Bove, Docent Phone: (46)(31) 772 1020 http://www.cse.chalmers.se/~bove Department of Computer Science and Engineering Chalmers Univ. of Technology and Univ. of Gothenburg -------------- next part -------------- An HTML attachment was scrubbed... URL: From abela at chalmers.se Sat Feb 24 12:20:17 2024 From: abela at chalmers.se (Andreas Abel) Date: Sat, 24 Feb 2024 12:20:17 +0100 Subject: [Agda] [ANNOUNCE] Agda 2.6.4.2 In-Reply-To: References: Message-ID: <6d58b9e1-14d2-40f5-8311-2225e261830d@chalmers.se> Dear all, The Agda Team is pleased to announce the release of Agda 2.6.4.2. Agda 2.6.4.2 is a bugfix release over Agda 2.6.4.1: - Fix an inconsistency in Cubical Agda related to catch-all clauses. - Fix some internal errors. - Fix an issue with `opaque`. - Fix building with cabal flag `-f debug-serialisation`. # GHC supported versions Agda 2.6.4.2 has been tested with GHC 9.8.1, GHC 9.6.4, 9.4.8, 9.2.8, 9.0.2, 8.10.7, 8.8.4 and 8.6.5 on Linux, macOS and Windows. # Installation Agda 2.6.4.2 can be installed using cabal-install or stack: 1. Getting the tarball $ cabal update $ cabal get Agda-2.6.4.2 $ cd Agda-2.6.4.2 2. a. Using cabal-install $ cabal install -f +optimise-heavily -f +enable-cluster-counting 2. b. Using stack $ stack --stack-yaml stack-a.b.c.yaml install --flag Agda:optimise-heavily --flag Agda:enable-cluster-counting replacing `a.b.c` with your version of GHC. The flags mean: - optimise-heavily: Turn on extra optimisation for a faster Agda. Takes large resources during compilation of Agda. - enable-cluster-counting: Enable unicode clusters for alignment in the LaTeX backend. Requires the ICU lib to be installed and known to pkg-config. These flags can be dropped from the install if causing trouble. # Standard library You can use standard library v1.7.3, v2.0 or the `master` branch of the standard library with Agda 2.6.4.2. This branch is available at https://github.com/agda/agda-stdlib/ # Fixed issues over Agda 2.6.4.1 https://hackage.haskell.org/package/Agda-2.6.4.2/candidate/changelog Enjoy Agda 2.6.4.2! Andreas, on behalf of the Agda Team -- Andreas Abel <>< Du bist der geliebte Mensch. Department of Computer Science and Engineering Chalmers and Gothenburg University, Sweden andreas.abel at gu.se http://www.cse.chalmers.se/~abela/ From paba at itu.dk Sun Feb 25 14:04:58 2024 From: paba at itu.dk (Patrick Bahr) Date: Sun, 25 Feb 2024 13:04:58 +0000 Subject: [Agda] TYPES 2024 - Call for Contributions Message-ID: <5DA0AEB6-BF25-4469-A811-524B6D828642@itu.dk> 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 at 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) From abela at chalmers.se Mon Feb 26 22:11:49 2024 From: abela at chalmers.se (Andreas Abel) Date: Mon, 26 Feb 2024 22:11:49 +0100 Subject: [Agda] [ANNOUNCE] Agda 2.6.4.2 retracted In-Reply-To: <6d58b9e1-14d2-40f5-8311-2225e261830d@chalmers.se> References: <6d58b9e1-14d2-40f5-8311-2225e261830d@chalmers.se> Message-ID: <554931ec-d2f4-4b8d-b25a-fe85a18b7fa9@chalmers.se> The Agda Team is not very pleased to announce that it has to retract Agda 2.6.4.2 due to a regression concerning `with`: https://github.com/agda/agda/issues/7148 So, please do not install it, wait for the next release. On 2024-02-24 12:20, Andreas Abel wrote: > Dear all, > > The Agda Team is pleased to announce the release of Agda 2.6.4.2. > > Agda 2.6.4.2 is a bugfix release over Agda 2.6.4.1: > > - Fix an inconsistency in Cubical Agda related to catch-all clauses. > - Fix some internal errors. > - Fix an issue with `opaque`. > - Fix building with cabal flag `-f debug-serialisation`. > > # GHC supported versions > > Agda 2.6.4.2 has been tested with GHC 9.8.1, GHC 9.6.4, 9.4.8, 9.2.8, > 9.0.2, 8.10.7, 8.8.4 and 8.6.5 on Linux, macOS and Windows. > > # Installation > > Agda 2.6.4.2 can be installed using cabal-install or stack: > > 1. Getting the tarball > > ??????? $ cabal update > ??????? $ cabal get Agda-2.6.4.2 > ??????? $ cd Agda-2.6.4.2 > > 2. a. Using cabal-install > > ????? $ cabal install -f +optimise-heavily -f +enable-cluster-counting > > 2. b. Using stack > > ????? $ stack --stack-yaml stack-a.b.c.yaml install --flag > Agda:optimise-heavily --flag Agda:enable-cluster-counting > > replacing `a.b.c` with your version of GHC. > > The flags mean: > > ? - optimise-heavily: > ??? Turn on extra optimisation for a faster Agda. > ??? Takes large resources during compilation of Agda. > > ? - enable-cluster-counting: > ??? Enable unicode clusters for alignment in the LaTeX backend. > ??? Requires the ICU lib to be installed and known to pkg-config. > > These flags can be dropped from the install if causing trouble. > > # Standard library > > You can use standard library v1.7.3, v2.0 or the `master` branch of the > standard library with Agda 2.6.4.2.? This branch is available at > > ? https://github.com/agda/agda-stdlib/ > > # Fixed issues over Agda 2.6.4.1 > > ? https://hackage.haskell.org/package/Agda-2.6.4.2/candidate/changelog > > Enjoy Agda 2.6.4.2! > > Andreas, on behalf of the Agda Team > -- Andreas Abel <>< Du bist der geliebte Mensch. Department of Computer Science and Engineering Chalmers and Gothenburg University, Sweden andreas.abel at gu.se http://www.cse.chalmers.se/~abela/ From andreas.abel at ifi.lmu.de Wed Feb 28 18:19:41 2024 From: andreas.abel at ifi.lmu.de (Andreas Abel) Date: Wed, 28 Feb 2024 18:19:41 +0100 Subject: [Agda] [ANN] Agda-2.6.4.3 release candidate 1 Message-ID: <29345156-dd4f-4912-b284-cc939766885c@ifi.lmu.de> Dear all, Ok, after the botched release of Agda 2.6.4.2 there is release candidate for Agda 2.6.4.3. Changes over Agda 2.6.4.2 are two fixes: - [Issue #7148](https://github.com/agda/agda/issues/7148): Regression in 2.6.4.2 concerning `with` - [Issue #7150](https://github.com/agda/agda/issues/7150): Regression in 2.6.4 in `rewrite` with instances # GHC supported versions Agda 2.6.4.3 RC 1 has been tested with GHC 9.8.1, GHC 9.6.4, 9.4.8, 9.2.8, 9.0.2, 8.10.7, 8.8.4 and 8.6.5 on Linux, macOS and Windows. # Installation Agda 2.6.4.3 RC 1 can be installed using cabal-install or stack: 1. Getting the release candidate $ cabal get https://hackage.haskell.org/package/Agda-2.6.4.3/candidate/Agda-2.6.4.3.tar.gz $ cd Agda-2.6.4.3 2. a. Using cabal-install $ cabal install -f +optimise-heavily -f +enable-cluster-counting 2. b. Using stack $ stack --stack-yaml stack-a.b.c.yaml install --flag Agda:optimise-heavily --flag Agda:enable-cluster-counting replacing `a.b.c` with your version of GHC. The flags mean: - optimise-heavily: Turn on extra optimisation for a faster Agda. Takes large resources during compilation of Agda. - enable-cluster-counting: Enable unicode clusters for alignment in the LaTeX backend. Requires the ICU lib to be installed and known to pkg-config. These flags can be dropped from the install if causing trouble. # Standard library You can use standard library v1.7.3, v2.0 or the `master` branch of the standard library with Agda 2.6.4.3. This branch is available at https://github.com/agda/agda-stdlib/ # Fixed issues over Agda 2.6.4.2 https://hackage.haskell.org/package/Agda-2.6.4.3/candidate/changelog Please test the Agda 2.6.4.3 RC 1 on your developments. Report problems and regressions to: https://github.com/agda/agda/issues Andreas, on behalf of the Agda Developers From Graham.Hutton at nottingham.ac.uk Mon Mar 4 10:10:51 2024 From: Graham.Hutton at nottingham.ac.uk (Graham Hutton) Date: Mon, 4 Mar 2024 09:10:51 +0000 Subject: [Agda] Midlands Graduate School (MGS) Message-ID: <456ADF99-5A0E-41DD-A141-50B4F3A76FDD@nottingham.ac.uk> Dear all, There are just a few days left now to register for this years Midlands Graduate School (MGS) in Leicester. Seven fantastic courses on category theory, proof theory, type theory, session types, and more. 8-12 April 2024, Leicester, UK. Registration closes Friday 8th March. Best wishes, Graham Hutton ========================================================== 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. ========================================================== ? Professor Graham Hutton School of Computer Science University of Nottingham, UK http://www.cs.nott.ac.uk/~pszgmh This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law. From tdejong.ac at gmail.com Mon Mar 4 10:54:41 2024 From: tdejong.ac at gmail.com (Tom de Jong) Date: Mon, 4 Mar 2024 09:54:41 +0000 Subject: [Agda] HoTT/UF 2024: Registration closing soon Message-ID: ========================================================== * Registration deadline: Friday 8 March * Talk schedule online Workshop on Homotopy Type Theory and Univalent Foundations (HoTT/UF) April 2 - 4, 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 as is the schedule of talks. ================ # 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 at gu.se (University of Gothenburg) * Tom de Jong, tom.dejong at nottingham.ac.uk (University of Nottingham) * Mitchell Riley, mitchell.v.riley at nyu.edu (NYU Abu Dhabi) * Jonathan Weinberger, jweinb20 at jhu.edu (Johns Hopkins University) From paba at itu.dk Tue Mar 5 14:32:48 2024 From: paba at itu.dk (Patrick Bahr) Date: Tue, 5 Mar 2024 13:32:48 +0000 Subject: [Agda] TYPES 2024: Call for Contributions - Deadline extension Message-ID: <1BC19ADA-0946-49DB-943B-B91C624A2783@itu.dk> 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 at 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) From andreas.abel at ifi.lmu.de Wed Mar 6 11:56:19 2024 From: andreas.abel at ifi.lmu.de (Andreas Abel) Date: Wed, 6 Mar 2024 11:56:19 +0100 Subject: [Agda] [ANN] Agda-2.6.4.3 Message-ID: <807ac15d-7713-4d0a-a44e-0688fb1e3126@ifi.lmu.de> Agda 2.6.4.3 has been released to replace the deprecated 2.6.4.2. Changes over Agda 2.6.4.2 are two fixes: - [Issue #7148](https://github.com/agda/agda/issues/7148): Regression in 2.6.4.2 concerning `with` - [Issue #7150](https://github.com/agda/agda/issues/7150): Regression in 2.6.4 in `rewrite` with instances # GHC supported versions Agda 2.6.4.3 has been tested with GHC 9.8.1, GHC 9.6.4, 9.4.8, 9.2.8, 9.0.2, 8.10.7, 8.8.4 and 8.6.5 on Linux, macOS and Windows. # Installation Agda 2.6.4.3 can be installed using cabal-install or stack: 1. Getting the release candidate $ cabal get https://hackage.haskell.org/package/Agda-2.6.4.3/Agda-2.6.4.3.tar.gz $ cd Agda-2.6.4.3 2. a. Using cabal-install $ cabal install -f +optimise-heavily -f +enable-cluster-counting 2. b. Using stack $ stack --stack-yaml stack-a.b.c.yaml install --flag Agda:optimise-heavily --flag Agda:enable-cluster-counting replacing `a.b.c` with your version of GHC. The flags mean: - optimise-heavily: Turn on extra optimisation for a faster Agda. Takes large resources during compilation of Agda. - enable-cluster-counting: Enable unicode clusters for alignment in the LaTeX backend. Requires the ICU lib to be installed and known to pkg-config. These flags can be dropped from the install if causing trouble. # Standard library You can use standard library v1.7.3, v2.0 or the `master` branch of the standard library with Agda 2.6.4.3. This branch is available at https://github.com/agda/agda-stdlib/ # Fixed issues over Agda 2.6.4.2 https://hackage.haskell.org/package/Agda-2.6.4.3/changelog Enjoy Agda! Report problems and regressions to: https://github.com/agda/agda/issues Andreas, on behalf of the Agda Developers From kbh at umn.edu Thu Mar 7 07:59:39 2024 From: kbh at umn.edu (Favonia) Date: Thu, 7 Mar 2024 00:59:39 -0600 Subject: [Agda] MSFP 2024 Call for Papers (short abstracts 26 Apr, papers 30 Apr) Message-ID: 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 at umn.edu) and Jeremy Gibbons (jeremy.gibbons at 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 -------------- next part -------------- An HTML attachment was scrubbed... URL: From xu at math.lmu.de Tue Mar 12 06:00:21 2024 From: xu at math.lmu.de (xu at math.lmu.de) Date: Tue, 12 Mar 2024 06:00:21 +0100 Subject: [Agda] Autumn school "Proof and Computation", Fischbachau (Germany), 15-21 Sep 2024 Message-ID: <20240312060021.Horde.7_MUmespmUPVNQbJMMyZKSg@webmail.mathematik.uni-muenchen.de> [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 . 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 From fredrik.nordvall-forsberg at strath.ac.uk Thu Mar 14 17:08:35 2024 From: fredrik.nordvall-forsberg at strath.ac.uk (Fredrik Nordvall Forsberg) Date: Thu, 14 Mar 2024 16:08:35 +0000 Subject: [Agda] Postdoc position at the University of Strathclyde Message-ID: 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 From A.G.Setzer at Swansea.ac.uk Fri Mar 15 14:25:56 2024 From: A.G.Setzer at Swansea.ac.uk (Anton Setzer) Date: Fri, 15 Mar 2024 13:25:56 +0000 Subject: [Agda] Agda Implementors' Meeting XXXVIII: Call for talks and participation Message-ID: Dear all, The thirty-eighth Agda Implementors' Meeting will take place in Swansea, Wales, UK from Monday 13 to Saturday 18 May 2024. Wiki link for more details: https://wiki.portal.chalmers.se/agda/Main/AIMXXXVIII The meeting aims to bring together people not only developing but also using Agda or even those who are simply interested in it. We will have talks on the implementation details of Agda in the morning and code sprints in the afternoon. You can still submit your proposal for a talk or discussion! There's a (soft) deadline for registration on 14 April 2024 Registration instructions: https://wiki.portal.chalmers.se/agda/Main/AIMXXXVIII#Registration Anton Setzer ----------------------------------------------------------------------------- Dr Anton Setzer Darllenydd / Reader Ystafell / Room 403 Adran Gyfrifiadureg / Dept. of Computer Science Y Ffowndri Gyfrifiadurol / Computational Foundry Coleg Gwyddoniaeth / College of Science Prifysgol Abertawe/ Swansea University Campws y Bae/ Bay Campus Abertawe / Swansea SA1 8EN DU / UK Rhowch wybod i ni os hoffech dderbyn eich gohebiaeth yn Gymraeg. / Let us know if you would like to receive correspondence in Welsh. Rydym yn croesawu gohebiaeth yn Gymraeg neu yn Saesneg. / We welcome correspondence in Welsh or English. Ni fydd gohebu yn Gymraeg yn arwain at oedi./ Corresponding in Welsh will not lead to a delay. -------------- next part -------------- An HTML attachment was scrubbed... URL: From ufarooq at lsu.edu Fri Mar 15 22:40:21 2024 From: ufarooq at lsu.edu (Umar Farooq) Date: Fri, 15 Mar 2024 21:40:21 +0000 Subject: [Agda] Call for Papers: OOPSLA 2024 Message-ID: ======================================================================== PACMPL Issue OOPSLA 2024 Call for Papers OOPSLA 2024 will be held as part of The ACM Conference on Systems, Programming, Languages, and Applications: Software for Humanity (SPLASH'24) October 20-25, 2024, Pasadena, California, United States https://2024.splashcon.org/track/splash-2024-oopsla ======================================================================== ### Important dates #### ROUND 2: Submission Deadline: Fri Apr 5, 2024 Author Response: Mon Jun 3 - Wed Jun 5, 2024 Author Notification: Fri Jun 21, 2024 Artifact Submission: Fri Jul 5, 2024 Artifact kick-tires: Sat Jul 6 - Fri Jul 19, 2024 Submission of Revisions: Sun Aug 4, 2024 Author Notification of Revisions: Sun Aug 18, 2024 Artifact Notification: Fri Aug 23, 2024 Camera Ready: Sun Sep 1, 2024 Papers accepted at either of the rounds will be published in the 2024 volume of PACMPL(OOPSLA) and invited to be presented at the SPLASH conference in October 2024. ### Scope The OOPSLA issue of the Proceedings of the ACM on Programming Languages (PACMPL) welcomes papers focusing on all practical and theoretical investigations of programming languages, systems and environments. Papers may target any stage of software development, including requirements, modelling, prototyping, design, implementation, generation, analysis, verification, testing, evaluation, maintenance, and reuse of software systems. Contributions may include the development of new tools, techniques, principles, and evaluations. #### Review Process PACMPL(OOPSLA) has two rounds of reviewing with submission deadlines around October and April each year. As you submit your paper you will receive around three reviews and an opportunity to provide an author response that will be read and addressed by the reviewers in the final decision outcome summary. There are 5 possible outcomes at the end of the round: *Accept*: Your paper will appear in the upcoming volume of PACMPL (OOPSLA). *Conditional Accept*: You will receive a list of required revisions that you will need to address. You must submit a revised paper, a clear explanation of how your revision addresses these comments, and "if possible" a diff of the PDF as supplementary material. Assuming you meet the listed requirements, after further review by the same reviewers, your paper will very likely be accepted. This process *has to be completed within two months of the initial decision* for the paper to be accepted, so we encourage timely turnaround in case revisions take more than one cycle to be accepted. *Minor Revision*: The reviewers have concerns that go beyond what can be enumerated in a list. Therefore, while you may receive a list of revisions suggested by the reviewers, this will not necessarily be comprehensive. You will have the opportunity to resubmit your revised paper and have it re-reviewed by the same reviewers, which may or may not result in your paper's acceptance. When you resubmit, you should clearly explain how the revisions address the comments of the reviewers, by including a document describing the changes and "if possible" a diff of the PDF as supplementary material. This process *has to be completed within two months of the initial decision* for the paper to be accepted in the current round, so we encourage timely turnaround in case revisions take more than one cycle to be accepted. *Major Revision*: You will receive a list of revisions suggested by the reviewers. Papers in this category are *invited to submit a revision to the next round of submissions* with a specific set of expectations to be met. When you resubmit, you should clearly explain how the revisions address the comments of the reviewers, by including a document describing the changes and "if possible" a diff of the PDF as supplementary material. The revised paper will be re-evaluated in the next round. Resubmitted papers will retain the same reviewers throughout the process to the extent possible. *Reject*: Rejected papers will not be included in the upcoming volume of PACMPL(OOPSLA). Papers in this category are not guaranteed a review if resubmitted less than one year from the date of the original submission. A paper will be judged to be a resubmission if it is substantially similar to the original submission. The Chairs will decide whether or not a paper is a resubmission of the same work. ### Submissions Submitted papers must be at most **23 pages** in 10 point font. There is no page limit on references. No appendices are allowed on the main paper, instead authors can upload supplementary material with no page or content restrictions, but reviewers may choose to ignore it. Submissions must adhere to the "ACM Small" template available from [the ACM](http://www.acm.org/publications/authors/submissions). Papers are expected to use author-year citations. Author-year citations may be used as either a noun phrase, such as "The lambda calculus was originally conceived by Church (1932)", or a parenthetic phase, such as "The lambda calculus (Church 1932) was intended as a foundation for mathematics". PACMPL uses double-blind reviewing. Authors' identities are only revealed if a paper is accepted. Papers must 1. omit author names and institutions, 2. use the third person when referencing your work, 3. anonymise supplementary material. Nothing should be done in the name of anonymity that weakens the submission; see the DBR FAQ. When in doubt, contact the Review Committee Chairs. Papers must describe unpublished work that is not currently submitted for publication elsewhere as described by [SIGPLAN's Republication Policy](http://www.sigplan.org/Resources/Policies/Republication). Submitters should also be aware of [ACM's Policy and Procedures on Plagiarism](http://www.acm.org/publications/policies/plagiarism_policy). Submissions are expected to comply with the [ACM Policies for Authorship](https://www.acm.org/publications/authors/information-for-authors). #### Artifacts Authors should indicate with their initial submission if an artifact exists, describe its nature and limitations, and indicate if it will be submitted for evaluation. Accepted papers that fail to provide an artifact will be requested to explain the reason they cannot support replication. It is understood that some papers have no artifacts. Please note that the artifact submission deadline will be following closely the paper submission deadline so make sure you check the Artifact Call as soon as you submit your paper to PACMPL(OOPSLA). ##### Data-Availability Statement To help readers find data and software, OOPSLA recommends adding a section just before the references titled Data-Availability Statement. If the paper has an artifact, cite it here. If there is no artifact, this section can explain how to obtain relevant code. The statement does not count toward the OOPSLA 2024 page limit. It may be included in the submitted paper; in fact we encourage this, even if the DOI is not ready yet. Example: \section{Conclusion} .... \section*{Data-Availability Statement} The software that supports~\cref{s:design,s:evaluation} is available on Software Heritage~\cite{artifact-swh} and Zenodo~\cite{artifact-doi}. \begin{acks} .... #### Expert PC Members During the submission, we will ask you to list up to 3 non-conflicted PC members who you think are experts on the topic of this submission, starting with the most expert. This list will not be used as an input during the paper assignment and it will not be visible to the PC. It may be used by the PC Chair and Associate Chairs for advice on external experts if the paper lacks expert reviews. ### Publication PACMPL is a Gold Open Access journal, all papers will be freely available to the public. Authors can voluntarily cover the article processing charge ($400 USD), but payment is not required. The official publication date is the date the journal is made available in the ACM Digital Library. The journal issue and associated papers may be published up to two weeks prior to the first day of the conference. The official publication date affects the deadline for any patent filings related to published work. By submitting your article to an ACM Publication, you are acknowledging that you and your co-authors are subject to all [ACM Publications Policies](https://www.acm.org/publications/policies), including ACM?s [new Publications Policy on Research Involving Human Participants and Subjects](https://www.acm.org/publications/policies/research-involving-human-participants-and-subjects). Alleged violations of this policy or an ACM Publications Policy will be investigated by ACM and may result in a full retraction of your paper, in addition to other potential penalties, as per ACM Publications Policy. Please ensure that you and your co-authors obtain [an ORCID ID](https://orcid.org/register), so you can complete the publishing process for your accepted paper. ACM has been involved in ORCID from the start and we have recently made a [commitment to collect ORCID IDs from all of our published authors](https://authors.acm.org/author-resources/orcid-faqs). We are committed to improving author discoverability, ensuring proper attribution and contributing to ongoing community efforts around name normalization; your ORCID ID will help in these efforts. The ACM Publications Board has recently updated the ACM Authorship Policy in several ways: - Addressing the use of generative AI systems in the publications process - Clarifying criteria for authorship and the responsibilities of authors - Defining prohibited behaviour, such as gift, ghost, or purchased authorship - Providing a linked FAQ explaining the rationale for the policy and providing additional details You can find the updated policy here: [https://www.acm.org/publications/policies/new-acm-policy-on-authorship](https://www.acm.org/publications/policies/new-acm-policy-on-authorship) ##### Review Committee Review Committee Chairs: Alex Potanin, Australian National University, Australia Bor-Yuh Evan Chang, University of Colorado Boulder, USA Review Committee Associate Chairs: Anders M?ller, Aarhus University, Denmark Lingming Zhang, UIUC, USA Review Committee: Aleksandar Nanevski, IMDEA Software Institute, Spain Alex Summers, University of British Columbia, Canada Alexandra Bugariu, ETH Zurich, Switzerland Ana Milanova, Rensselaer Polytechnic Institute, USA Andreas Zeller, CISPA Helmholtz Center for Information Security, Germany Anitha Gollamudi, UMass, USA Ankush Desai, AWS, USA Ashish Tiwari, Microsoft Research, USA Ben Hermann, TU Dortmund, Germany Ben Titzer, CMU, USA Benjamin Delaware, Purdue University, USA Bernardo Toninho, Universidade Nova de Lisboa, Portugal Bruno C. d. S. Oliveira, U. Hong Kong, Hong Kong Burcu Kulahcioglu Ozkan, Delft University of Technology, The Netherlands Casper Bach Poulsen, Delft University of Technology, Netherlands Colin Gordon, Drexel University, USA Corina Pasarenau, NASA, USA Cyrus Omar, University of Michigan, USA Damien Zufferey, Sonar Source, Switzerland Dana Drachsler Cohen, Technion, Israel David Darais, Galois, USA David Pearce, ConsenSys, New Zealand Di Wang, Peking University, China Emma S?derberg, Lund University, Sweden Emma Tosch, Northeastern University, USA Fabian Muehlboeck, Australian National University, Australia Fei He, Tsinghua University, China Filip Niksic, Google, USA Fredrik Kjolstad, Stanford University, USA Guido Salvaneschi, University of St. Gallen, Switzerland Hila Peleg, Technion, Israel Jiasi Shen, The Hong Kong University of Science and Technology, China (Hong Kong) Jonathan Bell, Northeastern University, USA Jonathan Brachth?user, University of T?bingen, Germany Joseph Tassarotti, New York University, USA Justin Hsu, Cornell University, USA Karine Even-Mendoza, King's College London, UK Kenji Maillard, Inria Rennes, France Matthew Flatt, U. Utah, USA Matthew Parkinson, Microsoft, UK Max Schaefer, GitHub, UK Michael Coblenz, UCSD, USA Milos Gligoric, UT Austin, USA Minseok Jeon, Korea University, Korea Mohamed Faouzi Atig, Uppsala University, Sweden Owolabi Legunsen, Cornell University, USA Pamela Zave, AT&T Laboratories, USA Pavel Panchekha, University of Utah, USA Rahul Gopinath, University of Sydney, Australia Rajiv Gupta, UC Riverside, USA Saman Amarasinghe, MIT, USA Santosh Pande, Georgia Institute of Technology, USA Sean Treichler, NVIDIA, USA Shachar Itzhaky, Technion, Israel Shaz Qadeer, Facebook, USA Sheng Chen, University of Louisiana at Lafayette, USA Shigeru Chiba, University of Tokyo, Japan Shriram Krishnamurthi, Brown University, USA Sreepathi Pai, University of Rochester, USA Stefan Brunthaler, University of the Federal Armed Forces in Munchen, Germany Steve Blackburn, Google, Australia Subhajit Roy, IIT Kanpur, India Sukyoung Ryu, KAIST, Korea Swarnendu Biswas, IIT Kanpur, India Thanh Vu Nguyen, George Mason University, USA Tiark Rompf, Purdue, USA Tien Nguyen, University of Texas at Dallas, USA Tomas Petricek, Charles University, Czech Republic Umut Acar, CMU, USA Wei Le, Iowa State, USA Wei Zhang , Meta, USA Xiaokang Qiu, Purdue University, USA Yingfei Xiong, Peking University, China Yizhou Zhang, University of Waterloo, Canada Youyou Cong, Tokyo Institute of Technology, Japan Yu David Liu, Binghamton, USA Yu Feng, UCSB, USA Yuepeng Wang, Simon Fraser University, Canada ##### Artifact Evaluation Committee Artifact Evaluation Committee Chairs: Guillaume Baudart, Inria - ?cole normale sup?rieure, France Sankha Narayan Guria, University of Kansas, USA -------------- next part -------------- An HTML attachment was scrubbed... URL: From tarmo at cs.ioc.ee Sat Mar 16 16:00:34 2024 From: tarmo at cs.ioc.ee (Tarmo Uustalu) Date: Sat, 16 Mar 2024 15:00:34 +0000 Subject: [Agda] Postdoc positions in Reykjavik Message-ID: <20240316150034.0f194712@kan> Two one-year postdoc positions (one possibly extendible to 1.5 years) are available in the ICE-TCS lab of the Department of Computer Science of Reykjavik University (https://www.ru.is/). One position is in the Icelandic Research Fund research project on computational effects and high-level control. In this project, we study in particular effectful concurrency and event-drivenness. These are the topics where we expect the postdoc to make research contributions. The other is in the University Collaboration Fund project to advance and promote computer-assisted proof in Iceland, in particular to introduce this technology to CS and math teaching at Reykjavik University and the University of Iceland. The postdoc has to prepare teaching material on verification of algorithms and datastructures in a type-theoretic proof assistant and teach from it, but there is also room for research in this domain. Start date: soonest, summer/autumn 2024. The gross salary is 663000 ISK (~4420 EUR) per month which amounts to ~3210 EUR after tax, with tax relief for foreign experts ~3675 EUR after tax. For closer information on the two projects as well as the research environment and the conditions of the contract, please get in touch with Tarmo Uustalu, firstname at ru . is. To apply, please send me a motivation letter explaining your background and interests together with your CV (including the names of two references) and copies of degree certificates latest by 31 March 2024. From w.s.swierstra at uu.nl Tue Mar 19 11:00:18 2024 From: w.s.swierstra at uu.nl (Wouter Swierstra) Date: Tue, 19 Mar 2024 11:00:18 +0100 Subject: [Agda] PhD position in Utrecht Message-ID: <18f02ddf-c389-499e-8497-c8ef2932ba9c@uu.nl> Dear all, Johan Commelin, Jim Portegies, and Paige North are looking for a PhD student to work on the development of proof assistants for education such as Waterproof [1] (see [2] for a project description). The position will be based at the Utrecht University (though it will also include collaboration with the Technical University of Eindhoven) and will start in Fall 2024. We will consider applications until the position has been filled. Please contact Paige at p.r.north at uu.nl if you are interested. All the best, Wouter [1] https://impermeable.github.io [2] https://paigenorth.github.io/tue-uu-project.pdf From w.s.swierstra at uu.nl Tue Mar 19 11:26:18 2024 From: w.s.swierstra at uu.nl (Wouter Swierstra) Date: Tue, 19 Mar 2024 11:26:18 +0100 Subject: [Agda] Utrecht Summer School on Advanced Functional Programming Message-ID: <17476886-7329-4622-a01b-acf540e0f82f@uu.nl> # Call for Participation SUMMER SCHOOL ON ADVANCED FUNCTIONAL PROGRAMMING Utrecht, the Netherlands, 08 July ? 12 July 2024 http://www.afp.school **Please register before June 1st ** ## ABOUT The Advanced Functional Programming summer school has been running for more than ten years. We aim to educate aspiring Haskell programmers beyond the basic material covered by many textbooks. The lectures will cover several more advanced topics regarding the theory and practice of Haskell programming, including topics such as: * lambda calculus; * monads and monad transformers; * lazy evaluation; * generalized algebraic data types; * type families and type-level programming; * concurrency and parallelism. The summer school will be held in Utrecht and consists of a mix of lectures, labs, and a busy social program. ## PREREQUISITES We expect students to have a basic familiarity with Haskell already. You should be able to write recursive functions over algebraic data types, such as lists and trees. There is a great deal of material readily available that covers this material. If you've already started learning Haskell and are looking to take your functional programming skills to the next level, this is the course for you. ## DATES **Registration deadline: June 1st, 2024** School: 08 July ? 12 July 2024 ## COSTS 750 euro - Profession registration fee 250 euro - Student registration fee 200 euro - Housing fee We will charge a registration fee of 750 euros (or 250 euros for students) to cover our expenses. If this is problematic for you for any reason at all, please email the organisers and we can try to offer you a discounted rate or a fee waiver. We have a limited number of scholarships or discounts available for students that would not be able to attend otherwise, especially for women and under-represented minorities. ## FURTHER INFORMATION Further information, including instructions on how to register, is available on our website: http://www.afp.school From kaposi.ambrus at gmail.com Wed Mar 20 16:23:53 2024 From: kaposi.ambrus at gmail.com (Ambrus Kaposi) Date: Wed, 20 Mar 2024 16:23:53 +0100 Subject: [Agda] Call for ITC conference grants, deadline 1 May 2024 Message-ID: <87a5mtexkm.fsf@neumann.mail-host-address-is-not-set> COST Action CA20111 EuroProofNet Open call for Inclusive Target Conference Grants (ITCGs) Dear Action members, The next deadline for ITCG proposals is: 1 May 2024 *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 Short Term Scientific Missions (STSMs). The conference should be between June and September 2024. The list of ITC countries is available at https://europroofnet.github.io/eligibility/ 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 From jesper at sikanda.be Mon Mar 25 14:48:14 2024 From: jesper at sikanda.be (Jesper Cockx) Date: Mon, 25 Mar 2024 13:48:14 +0000 Subject: [Agda] TyDe 2024: First call for papers and extended abstracts Message-ID: ========================================================================= The Ninth International Workshop on TYPE-DRIVEN DEVELOPMENT Call for papers and extended abstracts Milan, Italy, 6 September 2024 https://icfp24.sigplan.org/home/tyde-2024 ========================================================================= The Workshop on Type-Driven Development (TyDe) aims to show how static type information may be used effectively in the development of computer programs. Co-located with ICFP, this workshop brings together leading researchers and practitioners who are using or exploring types as a means of program development. We welcome all contributions, both theoretical and practical, on a range of topics including: * dependently typed programming; * generic programming; * design and implementation of programming languages, exploiting types in novel ways; * exploiting typed data, data dependent data, or type providers; * static and dynamic analyses of typed programs; * tools, IDEs, or testing tools exploiting type information; * pearls, being elegant, instructive examples of types used in the derivation, calculation, or construction of programs. ### Important dates ### * Mon 27 May 2024 (AoE): Submission deadline for papers and extended abstracts * Wed 10 Jul 2024: Notification of acceptance * Wed 17 Jul 2024: Submission of camera-ready papers to ACM * Fri 6 Sep 2024: Workshop ### Proceedings and Copyright ### We will have formal proceedings for full-length papers, published by the ACM. Accepted papers will be included in the ACM Digital Library. Authors must grant ACM publication rights upon acceptance, but may retain copyright if they wish. Authors are encouraged to publish auxiliary material with their paper (source code, test data, and so forth). The proceedings will be freely available for download from the ACM Digital Library from one week before the start of the conference until two weeks after the conference. The official publication date is the date the papers are made available in the ACM Digital Library. This date may be up to two weeks prior to the first day of the conference. The official publication date affects the deadline for any patent filings related to published work. ### Submission Details ### Submissions should fall into one of two categories: * regular research papers (12 pages); * extended abstracts (3 pages). The bibliography will not be counted against the page limits for either category. Regular research papers are expected to present novel and interesting research results, and will be included in the formal proceedings. Extended abstracts should report work in progress that the authors would like to present at the workshop. Extended abstracts will be distributed to workshop attendees but will not be published in the formal proceedings. We welcome submissions from PC members (with the exception of the two co-chairs), but these submissions will be held to a higher standard. Submission is handled through HotCRP: > https://tyde24.hotcrp.com All submissions should be in portable document format (PDF) and formatted using the ACM SIGPLAN style guidelines: > https://www.sigplan.org/Resources/Author/ Note that submissions should use the new ?acmart? format and the two-column ?sigplan? subformat (not to be confused with the one-column ?acmsmall? subformat). Extended abstracts must be submitted with the label ?Extended Abstract? clearly in the title. ### Participant Support ### Student attendees with accepted papers can apply for a SIGPLAN PAC grant to help cover participation-related expenses. PAC also offers other support, such as for child-care expenses during the meeting or for accommodations for members with physical disabilities. For details on the PAC program, see its web page: > https://www.sigplan.org/PAC/ -------------- next part -------------- A non-text attachment was scrubbed... Name: publickey - jesper at sikanda.be - 0x42DD5655.asc Type: application/pgp-keys Size: 644 bytes Desc: not available URL: -------------- next part -------------- A non-text attachment was scrubbed... Name: signature.asc Type: application/pgp-signature Size: 249 bytes Desc: OpenPGP digital signature URL: From benoit.montagu at inria.fr Mon Mar 25 15:09:14 2024 From: benoit.montagu at inria.fr (Benoit Montagu) Date: Mon, 25 Mar 2024 15:09:14 +0100 Subject: [Agda] Volunteers for ICFP 2024 Artifact Evaluation Committee (AEC) Message-ID: <146521d2-bce5-4778-a34d-b349cf661fda@inria.fr> Dear all, We are looking for motivated people to be members of the ICFP 2024 Artifact Evaluation Committee (AEC). Students, researchers and people from the industry or the free software community are all welcome. The artifact evaluation process aims to improve the quality and reproducibility of research artifacts for ICFP papers. In case you want to nominate someone else (students, colleagues, etc.), please send them the nomination form. Nomination form: ? https://forms.gle/KJAjtDzhm5VLxjVf9 Deadline for nominations: ? Mon April 8th 2024 For more information, see the AEC webpage: ? https://icfp24.sigplan.org/track/icfp-2024-artifact-evaluation The primary responsibility of committee members is to review the artifacts submitted corresponding to the already conditionally accepted papers in the main research track. In particular, run the associated tool or benchmark, check whether the results in the paper can be reproduced, and inspect the tool and the data. We expect evaluation of one artifact to take about a full day. Each committee member will receive 2 to 3 artifacts to review. All of the AEC work will be done remotely/online. The AEC will work in June, with the review work happening between June 5th and July 5th. Come join us in improving the quality of research in our field! Best, the Artifact Evaluation chairs: Quentin Sti?venart and Beno?t Montagu From A.G.Setzer at Swansea.ac.uk Wed Apr 3 12:31:10 2024 From: A.G.Setzer at Swansea.ac.uk (Anton Setzer) Date: Wed, 3 Apr 2024 10:31:10 +0000 Subject: [Agda] Agda Implementors' Meeting XXXVIII: Call for talks and participation Message-ID: Dear all, This is a reminder that the thirty-eighth Agda Implementors' Meeting will take place in Swansea, Wales, UK from Monday 13 to Saturday 18 May 2024. Wiki link for more details: https://wiki.portal.chalmers.se/agda/Main/AIMXXXVIII The meeting aims to bring together people not only developing but also using Agda or even those who are simply interested in it. We will have talks on the implementation details of Agda in the morning and code sprints in the afternoon. You can still submit your proposal for a talk or discussion! There's a (soft) deadline for registration on 14 April 2024 Registration instructions: https://wiki.portal.chalmers.se/agda/Main/AIMXXXVIII#Registration Anton Setzer ----------------------------------------------------------------------------- Dr Anton Setzer Darllenydd / Reader Ystafell / Room 403 Adran Gyfrifiadureg / Dept. of Computer Science Y Ffowndri Gyfrifiadurol / Computational Foundry Coleg Gwyddoniaeth / College of Science Prifysgol Abertawe/ Swansea University Campws y Bae/ Bay Campus Abertawe / Swansea SA1 8EN DU / UK Rhowch wybod i ni os hoffech dderbyn eich gohebiaeth yn Gymraeg. / Let us know if you would like to receive correspondence in Welsh. Rydym yn croesawu gohebiaeth yn Gymraeg neu yn Saesneg. / We welcome correspondence in Welsh or English. Ni fydd gohebu yn Gymraeg yn arwain at oedi./ Corresponding in Welsh will not lead to a delay. -------------- next part -------------- An HTML attachment was scrubbed... URL: From mukeshtiwari.iiitm at gmail.com Mon Apr 8 10:04:50 2024 From: mukeshtiwari.iiitm at gmail.com (mukesh tiwari) Date: Mon, 8 Apr 2024 09:04:50 +0100 Subject: [Agda] Agda Implementors' Meeting XXXVIII: Call for talks and participation Message-ID: Dear all, The thirty-eighth Agda Implementors' Meeting will take place in Swansea, Wales, UK from Monday 13 to Saturday 18 May 2024. Wiki link for more details: https://wiki.portal.chalmers.se/ agda /Main/AIMXXXVIII The meeting aims to bring together people not only developing but also using Agda or even those who are simply interested in it. We will have talks on the implementation details of Agda in the morning and code sprints in the afternoon. You can still submit your proposal for a talk or discussion! There's a (soft) deadline for registration on 14 April 2024 Registration instructions: https://wiki.portal.chalmers.se/ agda /Main/AIMXXXVIII#Registration Best wishes, Anton Setzer ----------------------------------------------------------------------------- Dr Anton Setzer Darllenydd / Reader Ystafell / Room 403 Adran Gyfrifiadureg / Dept. of Computer Science Y Ffowndri Gyfrifiadurol / Computational Foundry Coleg Gwyddoniaeth / College of Science Prifysgol Abertawe/ Swansea University Campws y Bae/ Bay Campus Abertawe / Swansea SA1 8EN DU / UK Rhowch wybod i ni os hoffech dderbyn eich gohebiaeth yn Gymraeg. / Let us know if you would like to receive correspondence in Welsh. Rydym yn croesawu gohebiaeth yn Gymraeg neu yn Saesneg. / We welcome correspondence in Welsh or English. Ni fydd gohebu yn Gymraeg yn arwain at oedi./ Corresponding in Welsh will not lead to a delay. -------------- next part -------------- An HTML attachment was scrubbed... URL: From reuben.rowe at rhul.ac.uk Mon Apr 8 13:30:13 2024 From: reuben.rowe at rhul.ac.uk (Reuben Rowe) Date: Mon, 8 Apr 2024 12:30:13 +0100 Subject: [Agda] Agda Termination Checker Implements Size-Change Termination? Message-ID: Dear Agda List, Apologies if the answer to my question is by now folklore, but I could not find it through searching online, or by asking some colleagues who are Agda users. Q: Does the Agda termination checker in fact implement the check for size-change termination? [1] When I look at the Agda documentation for information about the termination checker, it points me towards Andreas' original technical report [2]. I have also looked at the subsequent formally published description, written with Thorsten [3]. Certainly, one can identify the call matrices of [2,3] with the size-change graphs of [1]. However, there is a difference between the lexicographic and termination orders of Defs 3.14 and 3.15 of [3], and the size-change termination property (Thm 4) of [1]. In particular, consider the following Agda function, 2-hydra-total, that encodes the standard cyclic proof of the totality of Berardi and Tatsuta's 2-hydra predicate [4]. open import Data.Nat using (?; zero; suc) -- The 2-Hydra predicate data 2-hydra : ? ? ? ? Set where base? : 2-hydra 0 0 base? : 2-hydra 1 0 base? : ?{n} ? 2-hydra n 1 step? : ?{n m} ? 2-hydra n m ? 2-hydra (suc n) (suc (suc m)) step? : ?{n} ? 2-hydra (suc n) n ? 2-hydra 0 (suc (suc n)) step? : ?{n} ? 2-hydra (suc n) n ? 2-hydra (suc (suc n)) 0 -- Totality of 2-hydra 2-hydra-total : ?(n m : ?) ? 2-hydra n m 2-hydra-total zero zero = base? 2-hydra-total (suc zero) zero = base? 2-hydra-total (suc (suc n)) zero = step? (2-hydra-total (suc n) n) 2-hydra-total n (suc zero) = base? 2-hydra-total zero (suc (suc m)) = step? (2-hydra-total (suc m) m) 2-hydra-total (suc n) (suc (suc m)) = step? (2-hydra-total n m) This does *not* have a termination ordering according to Def. 3.15 of [3]. The "recursion behaviour" of 2-hydra-total is the set B = {(<,<), (<,?), (?,<)}, and so there is no way to pick a permutation ? of the input parameters such that for all r ? B, r_?(0) ? ? (as required by Def. 3.14 of [3]). However, 2-hydra-total *does* satisfy the size-change termination condition (infinite descent in cyclic proofs is equivalent to the size-change termination property). Moreover, Agda happily reports that 2-hydra-total terminates. I did find a blog post (from 2018) discussing the termination checker [5], which demonstrates debug output from Agda talking about "Idempotent call matrices". This also suggests to me that the termination checker may be implementing size-change termination since, as formulated in [1], this requires checking properties of idempotent size-change graphs. (I wanted to reproduce this debug output in the version of Agda I am running - 2.6.3 - but the commands used in the blog post do not seem to produce this output anymore. Is there still a way to get Agda to output the call matrices produced by the termination checker?). Is there a more up-to-date published account of what Agda currently implements in the termination checker? I'd be very interested to know about this. Thanks, Reuben Rowe [1] Chin Soon Lee, Neil D. Jones, and Amir M. Ben-Amram: The Size-change Principle for Program Termination. In Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL '01). Association for Computing Machinery, New York, NY, USA, 81?92. (2001). https://doi.org/10.1145/360204.360210 [2] Andreas Abel: foetus - Termination Checker for Simple Functional Programs. https://www.cse.chalmers.se/~abela/foetus.pdf [3] Andreas Abel,Thorsten Altenkirch: A Predicative Analysis of Structural Recursion. Journal of Functional Programming. 2002;12(1):1?41. https://doi.org/10.1017/S0956796801004191 [4] Stefano Berardi, Makoto Tatsuta: Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proofs. Log. Methods Comput. Sci. 15(3) (2019). https://doi.org/10.23638/LMCS-15(3:10)2019 [5] Oleg Grenrus: Notes on Agda's Termination Checker. https://oleg.fi/gists/posts/2018-08-29-agda-termination-checker.html This email, its contents and any attachments are intended solely for the addressee and may contain confidential information. In certain circumstances, it may also be subject to legal privilege. Any unauthorised use, disclosure, or copying is not permitted. If you have received this email in error, please notify us and immediately and permanently delete it. Any views or opinions expressed in personal emails are solely those of the author and do not necessarily represent those of Royal Holloway, University of London. It is your responsibility to ensure that this email and any attachments are virus free. From edprocess at dline.info Tue Apr 9 08:21:54 2024 From: edprocess at dline.info (edprocess dline.info) Date: Tue, 9 Apr 2024 06:21:54 +0000 Subject: [Agda] Real-Time Intelligent Systems 2024 Message-ID: Sixth International Conference on Real-Time Intelligent Systems (RTIS 2024) Tien Giang University My Tho (near Ho-chi-Minh) Vietnam October 17-19, 2024 www.socio.org.uk/rtis Springer Lecture Notes in Networks and Systems (LNNS) The International Conference on Real-time Intelligent Systems (RTIS) has traveled from Beijing, China (2016), to Ho-Chi-Min, Vietnam. The sixth edition will take place at Tien Giang University. Over the last few years, real-time intelligent computing has radically transformed the human lifestyle. Research on real-time intelligent systems is multi-disciplinary, exploiting concepts from diverse areas such as big data processing, computational intelligence, location-based services, recommendation systems, and multimedia processing. In today?s highly dynamic environment, analysing data in real-time is necessary to understand how systems process data, reason the outputs, and anticipate trends in intelligent computing. To this end, this conference will serve as a platform to manifest the ongoing research in the field. Thus, RTIS welcomes theoretically grounded, methodologically sound papers that address aspects related to topics, such as: Artificial Intelligence and Data mining Streaming data, streaming engines Trace-based intelligent real-time services Adaptive vision algorithms Location-based services Intelligent Robotic Systems Collaborative Intelligence Data capture in real-time Data quality and cleansing Intelligent Data Analysis Intelligent Database Systems Knowledge representation and reasoning Intelligent information fusion Large Language Models, cognitive methods, sequential inference, data mining, pattern/behavioral analysis, Big Data systems and applications for high-velocity data Intelligent Information Systems Privacy and security in Intelligence Software Engineering Solutions Intelligent Soft Computing Real-time multiprocessor systems Internet of Things Architectures for Intelligence Real-time distributed coding Smart services and platforms Real-time modelling user information needs Wireless Communication Real-time intelligent communication Real-time intelligent network solutions Mobile Smart Systems Broadband Intelligence Cloud Computing and Intelligence Collaborative Intelligence Analysis in domains such as energy, sensors Decision support systems in real-time Multi-agent Intelligent Systems Multilingual information access Recommendation systems Real-time intelligent alert systems Real-time remote access systems Intelligent Transportation Systems Autonomous systems (incl. autonomous vehicles and drones) Distributed systems Cloud/edge computing/fusion Defence/security, robotics, aerospace, intelligent transportation Mining/Manufacturing Environmental monitoring Critical Real-time Applications Real-time noise removal systems Event-driven analytics Intelligent Fuzzy Systems Machine translation in real-time OLAP for real-time decision support Crowdsourcing and crowd intelligence Submission, proceedings Papers must be submitted online through OpenConf. Author instructions and LaTex2e (preferred) and Word macro files are available on the submission page. Submitted papers should be at most 14 pages (long papers) and 8 pages (short ones), including figures, tables and references (in the Springer template). Authors of accepted papers are required to transfer their copyrights. For a paper to appear in the proceedings, at least one of the authors MUST register for the conference by the camera-ready submission deadline with a full registration. Springer?s Lecture Notes in Networks and Systems (LNNS) (https://www.springer.com/series/15179) will publish the accepted papers and be indexed in SCOPUS, EI Compendex, INSPEC, WTI Frankfurt eG, zbMATH, and SCImago. All the papers published in the series are submitted for consideration in the Web of Science. Important Dates Submission of papers: August 05, 2024 Notification: September 01, 2024 Camera-ready: October 01, 2024 Registration: October 01, 2024 Conference Dates: October 17-19, 2024 Honorary Chair Vo Ngoc Ha, Tien Giang University, Vietnam General Chairs Le Minh Tung, Tien Giang University, Vietnam Mart?n L?PEZ-NORES, University of Vigo, Spain Program Chairs Nguyen Hoang Vu, Tien Giang University, Vietnam Pit Pichappan, Digital Information Research Labs, India & UK Dion Goh Hoe Lian, Nanyang Technological University, Singapore Co-Program Chairs Duong Van Hieu, Tien Giang University, Vietnam Ricardo Rodriguez-Jorge, Technological Centre Ceit, Spain Pavel Losket, Zhejiang University-University of Illinois at Urbana Champaign Institute, China Organizing Chair Cao Nguyen Thi, Tien Giang University, Vietnam Publicity Chair Beniysa Mohsin, LTI laboratory, Abdelmalek Essa?di University, Morocco Paper submission at https://socio.org.uk/rtis/paper-submission/ Contact stm at socio.org.uk -------------- next part -------------- An HTML attachment was scrubbed... URL: From alexis.saurin at irif.fr Fri Apr 12 19:23:46 2024 From: alexis.saurin at irif.fr (Alexis Saurin) Date: Fri, 12 Apr 2024 19:23:46 +0200 Subject: [Agda] Three Post-doc positions in RECIPROG project (located in France -- Lyon, Nantes and Paris) Message-ID: <40c39435ca5d736f93c11c1659bae0bf@irif.fr> This is an announcement for three one-year postdoctoral positions funded by the ANR ReCiProg - Reasoning on Circular proofs for Programming, to be hosted in Lyon (LIP), Nantes (LS2N, Gallinette) and Paris (IRIF, PPS). We seek strong candidates holding a PhD in Computer Science or Mathematics, and with expertise in one or several of the following areas: * Proof theory * Curry-Howard correspondence * Logics with fixed points * Coinductive reasoning * Proof assistants (formalization skills or development experience) * Type theory * Category theory * Automated deduction * Automata theory In relation with the above topics, an experience in one or several of the following topics will be particularly appreciated: fixed-points and circular proofs, the Coq proof assistant, inductive and coinductive types, guarded recursion, coalgebras, inductive and coinductive theorem proving, categorical logic, infinitary term rewriting and infinitary lambda-calculi. The successful candidate will be employed in one of the following French research lab, depending on her/his specific profile and scientific project: - LIP (Plume Team), Lyon (local coordinator: Denis Kuperberg) - LS2N (Gallinette Team), Nantes (local coordinator: Guilhem Jaber) - IRIF (PPS & Picube Team), Paris (local coordinator: Alexis Saurin) Application process: * Each potential candidate is advised to contact the project coordinator and the local coordinators of interest as soon as possible to express her/his intent to submit an application. * Deadline for applications is on May 15th, for a starting date between September 1st 2024 and December 31st 2024, to be negotiated. * Candidates should send their application to Alexis Saurin (alexis dot saurin at irif dot fr) with a subject containing "[RECIPROG post-doc application]". * The application should contain (i) a CV, (ii) a brief research statement (1-2 pages) & (iii) at least two contacts of reference persons (or reference letters if available) and it should indicate the site(s) of interest for the application. * The salary will depend on the successful candidate's prior research experience and of hiring site, with a guaranteed minimum of 2300 EUR/month before taxes. * Each position is for a one-year post-doc. Project summary: RECIPROG is an ANR collaborative project (aka. PRC) running till the end of 2025 involving french teams in Lyon, Marseille, Nantes and Marseille, which aims at extending the proofs-as-programs correspondence (aka Curry-Howard correspondence) to recursive programs and circular proofs for logics and type systems using induction and coinduction. The project will contribute both to the necessary theoretical foundations of circular proofs and to the software development allowing to enhance the use of coinductive types and coinductive reasoning in the Coq proof assistant, as well as software verification techniques using circular tools. More informations: * More informations can be found on the project webpage: https://www.irif.fr/reciprog/index and https://www.irif.fr/reciprog/post-doc-offer-paril-2024 * Interested candidates may contact the project coordinator (Alexis Saurin) as well as the local coordinators (Guilhem Jaber, Denis Kuperberg, Luigi Santocanale & Alexis Saurin) to enquire about more specific research directions and the adequacy of their research profile. * Cross-site projects involving members of the project from different labs are welcome. * There is a one-year funding for each of the three sites of Lyon, Nantes and Paris. -- Alexis Saurin IRIF - CNRS, Universit? Paris-Cit? & INRIA -------------- next part -------------- An HTML attachment was scrubbed... URL: From bove at chalmers.se Tue Apr 16 13:24:08 2024 From: bove at chalmers.se (Ana Bove) Date: Tue, 16 Apr 2024 13:24:08 +0200 Subject: [Agda] Two PhD positions in Computing science at Chalmers Message-ID: <42c93752-9b5b-410e-94ce-05e04dcc1edd@chalmers.se> Dear All The Computing science division at the department of Computer science and engineering, Chalmers, has two open PhD positions. I would appreciate if you can distribute the information to those you might think can be interested/are good candidates. ** Formal Verification of Autonomous Systems* The goal of the PhD project is to develop techniques for the design and verification of assured ACPS with a focus on runtime assurance. You will develop theory and tools for the construction of runtime monitors that capture under what conditions an ACPS is guaranteed to maintain safety. A key challenge in developing such monitors is to handle noisy, missing, or delayed data. Of particular interest is the investigation of compositional methods for constructing runtime monitors. _Deadline for application: April 30th _More information: https://www.chalmers.se/en/about-chalmers/work-with-us/vacancies/?rmpage=job&rmjob=12785&rmlang=UK ** Graph modification* The goal is to investigate the tractability of these problems from both the classical and parameterized complexity perspectives. This work lies at the intersection of structural graph theory, computational complexity and algorithm design. _Deadline for application: May 21st_ More information: https://www.chalmers.se/om-chalmers/arbeta-hos-oss/lediga-tjanster/?rmpage=job&rmjob=12806&rmlang=SE -- -- Ana Bove, Docent Phone: (46)(31) 772 1020 http://www.cse.chalmers.se/~bove Department of Computer Science and Engineering Chalmers Univ. of Technology and Univ. of Gothenburg -------------- next part -------------- An HTML attachment was scrubbed... URL: From paba at itu.dk Thu Apr 18 15:59:32 2024 From: paba at itu.dk (Patrick Bahr) Date: Thu, 18 Apr 2024 13:59:32 +0000 Subject: [Agda] TYPES 2024: Call for Participation Message-ID: Call for Participation TYPES 2024 30th International Conference on Types for Proofs and Programs Copenhagen, Denmark, 10 - 14 June 2024 https://types2024.itu.dk REGISTRATION ------------ Registration is now open at https://types2024.itu.dk/Registration.html * Early registration until May 13 * Late registration until May 30 Students can register at a reduced fee. For details, see the above link. ACCOMMODATION ------------ We have reserved a number of hotel rooms at reduced rates. * Some rooms are only available until April 24! A small number of rooms may be available as late as May 24, but supply is limited after April 24. We therefore encourage participants to book these soon. More details at https://types2024.itu.dk/Venue.html INVITED SPEAKERS ---------------- * Brigitte Pientka (McGill University, Canada) * Egbert Rijke (University of Ljubljana, Slovenia) * Talia Ringer (University of Illinois at Urbana-Champaign, USA) There will also be a special session in memory of Peter Aczel, organised by Peter Dybjer. The session will consist of talks by * Nicola Gambino (University of Manchester, UK) * Michael Rathjen (University of Leeds, UK) BACKGROUND ---------- 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. 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 at 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) From bove at chalmers.se Thu Apr 18 16:50:02 2024 From: bove at chalmers.se (Ana Bove) Date: Thu, 18 Apr 2024 16:50:02 +0200 Subject: [Agda] PhD position in neuro-symbolic AI for Mathematical Discovery Message-ID: <65674fd7-62fc-4f82-ac05-386e832670af@chalmers.se> Dear all, The Computer science and engineering department at Chalmers has a PhD position on *neuro-symbolic AI for Mathematical Discovery *with Assoc.Prof Moa Johansson as main supervisor and Prof. Thierry Coquand as co-supervisor. Please forward the information to those you think might be interested/good candidates. An ideal candidate is someone with interests and knowledge both in functional programming and machine learning. *Project description: *The goal of this project is to develop new methods for assisting mathematical discovery, by leveraging recent developments in generative AI (large language models) with symbolic systems (here proof-assistants) via a neuro-symbolic architecture. This takes advantage of AI systems with different strengths: generative AI-systems provide creativity, but are potentially unreliable and may hallucinate, while classical symbolic methods are rigid but reliable and can robustly check the correctness of results.* * *More information and application: *(deadline May 31st) https://www.chalmers.se/om-chalmers/arbeta-hos-oss/lediga-tjanster/?rmpage=job&rmjob=12851&rmlang=SE -- -- Ana Bove, Docent Phone: (46)(31) 772 1020 http://www.cse.chalmers.se/~bove Department of Computer Science and Engineering Chalmers Univ. of Technology and Univ. of Gothenburg -------------- next part -------------- An HTML attachment was scrubbed... URL: From mir.ikbch at gmail.com Fri Apr 19 04:21:04 2024 From: mir.ikbch at gmail.com (Mirai Ikebuchi) Date: Fri, 19 Apr 2024 11:21:04 +0900 Subject: [Agda] APLAS 2024: 2nd Call for Papers Message-ID: <07A9FB0A-24E0-4328-B767-63D0F7E991B7@gmail.com> 2nd Call for Papers APLAS 2024 -- The 22nd Asian Symposium on Programming Languages and Systems October 22-24, 2024, Kyoto, Japan https://conf.researchr.org/home/aplas-2024/ APLAS 2024 aims to bring together programming language researchers, practitioners and implementors *worldwide*, to present and discuss the latest results and exchange ideas in all areas of programming languages and systems. APLAS 2024 is co-located with the 22nd International Symposium on Automated Technology for Verification and Analysis (ATVA). We solicit submissions in the form of regular research papers describing original scientific research results, including system development and case studies. Among others, solicited topics include: programming paradigms and styles; methods and tools to specify and reason about programs and languages; programming language foundations; methods and tools for implementation; concurrency and distribution; applications, case studies and emerging topics. Submissions should not exceed 17 pages, excluding bibliography, in the Springer LNCS format. The reviewing process is light double-blind, with a rebuttal phase to address factual errors and minor misunderstandings. Proceedings of APLAS 2024 will be published by Springer as part of Lecture Notes in Computer Science (LNCS). https://link.springer.com/conference/aplas APLAS 2024 continues the tradition of the best paper award. Submission deadline: Fri May 24 Response period: Jul 24-26 Acceptance notification: Fri Aug 2 Camera-ready: Sat Aug 31 The submission website is now open: https://aplas24.hotcrp.com/ General Chair: Jacques Garrigue (Nagoya U.) Publicity Chairs: Ryosuke Sato (Tokyo U.), Mirai Ikebuchi (Kyoto U.) Program Committee: Beniamino Accattoli (Inria & Ecole Polytechnique) Pierre-Evariste Dagand (IRIF / CNRS) Silvia Ghilezan (University of Novi Sad, Mathematical Institute SASA) Fritz Henglein (DIKU and Deon Digital) Mirai Ikebuchi (Kyoto University) Patrik Jansson (Chalmers University of Technology and University of Gothenburg) Oleg Kiselyov (Tohoku University, PC Chair) Hsiang-Shang ?Josh? Ko (Academia Sinica) Daan Leijen (Microsoft Research) Martin Lester (University of Reading) Fredrik Nordvall Forsberg (University of Strathclyde) Matija Pretnar (University of Ljubljana) Peter Schachte (The University of Melbourne) Sven-Bodo Scholz (Radboud University) Philipp Schuster (University of T?bingen) Taro Sekiyama (NII) Amir Shaikhha (University of Edinburgh) Pavle Subotic (Fantom Foundation) Yong Kiam Tan (Institute for Infocomm Research, A*STAR) Kazunori Ueda (Waseda University) Yuting Wang (Shanghai Jiao Tong University) Ki Yung Ahn (Hannam University) -------------- next part -------------- An HTML attachment was scrubbed... URL: From kbh at umn.edu Sun Apr 21 16:33:50 2024 From: kbh at umn.edu (Favonia) Date: Sun, 21 Apr 2024 09:33:50 -0500 Subject: [Agda] Student Research Competition (SRC) at ICFP 2024 Message-ID: ICFP 2024 Student Research Competition Call for Submissions ICFP 2024 invites students to participate in the Student Research Competition in order to present their research and get feedback from prominent members of the programming language research community. The SRC consists of three rounds: * Submission of an extended abstract * Poster session at ICFP 2024 * Finalists' presentations at ICFP 2024 During the first round students submit an extended abstract detailing their research to be reviewed by the program committee. Those students whose abstracts get accepted advance to the poster session round which will take place during ICFP 2024. Winners of the poster session advance to the next round, where they will give a 5-minute presentation about their work on the ICFP main stage in front of a live audience. ### IMPORTANT DATES AND TIMES * Submission Deadline: 23 May 2024 (Thursday) * Author Notification: 14 June 2024 (Friday) 12:00 PM CST * ICFP 2024 Conference in Milan, Italy: 2 September 2024 (Monday) - 7 September 2024 (Saturday) ### SUBMISSION OF EXTENDED ABSTRACTS * Submission Website: https://icfp24src.hotcrp.com Each submission (referred to as "abstract" below) should include the student author's name and e-mail address; institutional affiliation; research advisor's name; ACM student member number; category (undergraduate or graduate); research title; and an extended abstract addressing the following: * Problem and Motivation: Clearly state the problem being addressed and explain the reasons for seeking a solution to this problem. * Background and Related Work: Describe the specialized (but pertinent) background necessary to appreciate the work in the context of ICFP areas of interest. Include references to the literature where appropriate, and briefly explain where your work departs from that done by others. * Approach and Uniqueness: Describe your approach in addressing the problem and clearly state how your approach is novel. * Results and Contributions: Clearly show how the results of your work contribute to programming language design and implementation in particular and to computer science in general; explain the significance of those results. * Submissions must be original research that is not already published at ICFP or another conference or journal. One of the goals of the SRC is to give students feedback on ongoing, unpublished work. Furthermore, the abstract must be authored solely by the student. If the work is collaborative with others and/or part of a larger group project, the abstract should make clear what the student's role was and should focus on that portion of the work. * Formatting: Submissions must be in PDF format, printable in black and white on US Letter sized paper, and interpretable by common PDF tools. All submissions must adhere to the "ACM Small" template that is available (in both LaTeX and Word formats) from https://www.acm.org/publications/authors/submissions. For authors using LaTeX, a lighter-weight package, including only the essential files, is available from http://sigplan.org/Resources/Author/#acmart-format. The submission must not exceed 3 pages in PDF format. Reference lists do not count towards the 3-page limit. Further information is available at the ICFP SRC website: https://icfp24.sigplan.org/track/icfp-2024-student-research-competition -------------- next part -------------- An HTML attachment was scrubbed... URL: From kbh at umn.edu Mon Apr 22 17:06:31 2024 From: kbh at umn.edu (Favonia) Date: Mon, 22 Apr 2024 10:06:31 -0500 Subject: [Agda] School on Univalent Mathematics, Minneapolis (MN, USA), July 29-Aug 2, 2024 Message-ID: We are pleased to announce the School on Univalent Mathematics 2024 to be held at the University of Minnesota (Twin Cities), Minneapolis, MN, United States, July 29-August 2, 2024 (https://unimath.github.io/minneapolis2024) If you are interested, please fill out the application form (https://forms.gle/9PTB2V19hVuJsidz8). We will start the reviewing on *May 6, 2024* and accept applicants on a rolling basis. Overview ======== Homotopy Type Theory is an emerging field of mathematics that studies a fruitful relationship between homotopy theory and (dependent) type theory. This relation plays a crucial role in Voevodsky's program of Univalent Foundations, a new approach to foundations of mathematics based on ideas from homotopy theory, such as the Univalence Principle. The UniMath library is a large repository of computer-checked mathematics, developed from the univalent viewpoint. It is based on the computer proof assistant Coq. In this school, we aim to introduce newcomers to the ideas of Univalent Foundations and mathematics therein, and to the formalization of mathematics in UniMath (https://github.com/UniMath/UniMath). This is our first school in the United States in the hope that students in North America can participate more easily. Format ======= Participants will receive an introduction to Univalent Foundations and to mathematics in those foundations. In the accompanying problem sessions, they will formalize pieces of univalent mathematics in the UniMath library. Prerequisites ========== Participants should be interested in mathematics and the use of computers for mathematical reasoning. Participants do not need to have prior knowledge of logic, Coq, or Univalent Foundations. Application and funding ======================= Please fill out the form (https://forms.gle/9PTB2V19hVuJsidz8). For information on how to participate, please visit https://unimath.github.io/minneapolis2024 Best regards, The organizers Benedikt Ahrens and Favonia From robby at racket-lang.org Thu Apr 25 20:06:42 2024 From: robby at racket-lang.org (Robby Findler) Date: Thu, 25 Apr 2024 13:06:42 -0500 Subject: [Agda] performance debugging? In-Reply-To: References: <6caeca26-377c-6704-e253-2003e8c7babd@cse.gu.se> Message-ID: Hi all-- This morning I was working on a lemma that really seems like it is taking longer than it should. I tried all the approaches that various folks sent me in this thread (lossy-unification, no-infer-absurd-clauses, opaque declarations -- thank you!) but, alas, was not able to get any improvements. (I'm not sure that I made the right definitions opaque, tho!). The lemma takes in two related arguments and, instead of being O(n^2) cases in the constructors, it is O(n) because of the relationship. Each time I load this lemma, it takes 7.5 minutes (using "time agda file.agda" on a file containing only this lemma whose imports are all already checked). After the initial case split, it was taking maybe 2-3 minutes to load the file (with each rhs just being a hole), in case that seems important. A different lemma that I was working on yesterday takes similar arguments except there is only one (not two) of these one arguments and I can work on that one at basically interactive speeds (just some seconds to load that lemma). According to the Emacs mode, the thing that takes most of the time is when the entire function is highlighted (not the individual cases, although those aren't speedy either). Assuming this description doesn't spark any ideas that others might have that I could try, I was wondering if anyone more versed in agda performance might be willing to have a look? I've trimmed down the development to just the file that has the overly slow lemma and its dependencies (it also depends on the iowa agda library, not the standard lib that comes with agda which I've not yet learned...). It is still pretty big, I'm sorry to say, at nearly 1800 lines (not counting what it uses in ial), but the file with the bad lemma is 118 lines. I don't think I'm doing anything particularly sophisticated in this code. (I'm no agda guru! :). tia, Robby -------------- next part -------------- An HTML attachment was scrubbed... URL: From nad at cse.gu.se Fri Apr 26 11:05:37 2024 From: nad at cse.gu.se (Nils Anders Danielsson) Date: Fri, 26 Apr 2024 11:05:37 +0200 Subject: [Agda] performance debugging? In-Reply-To: References: <6caeca26-377c-6704-e253-2003e8c7babd@cse.gu.se> Message-ID: <8452a6c3-c27d-4ea7-b5ad-2f259fe990ed@cse.gu.se> On 2024-04-25 20:06, Robby Findler wrote: > The lemma takes in two related arguments and, instead of being O(n^2) > cases in the constructors, it is O(n) because of the relationship. > According to the Emacs mode, the thing that takes most of the time is > when the entire function is highlighted (not the individual cases, > although those aren't speedy either). Your code may only contain "O(n)" cases, but I suspect that Agda still does some work to discard the remaining cases. I've recently optimised code with similar characteristics. Perhaps you can do something similar: * Prove suitable inversion lemmas for one of the two types. * Instead of matching on both arguments, match on one, and use inversion lemmas for the other argument. -- /NAD From kbh at umn.edu Fri Apr 26 16:18:31 2024 From: kbh at umn.edu (Favonia) Date: Fri, 26 Apr 2024 09:18:31 -0500 Subject: [Agda] Reminder: MSFP 2024 Call for Papers (deadline 30 Apr) Message-ID: This is a gentle reminder about the upcoming paper submission deadline for MSFP 2024: Tuesday 30th April, AoE. The original CFP did ask for abstracts in advance, but we will not insist on those: if you have a paper and have not registered an abstract, submit it anyway! Jeremy and Favonia * Tenth Workshop on MATHEMATICALLY STRUCTURED FUNCTIONAL PROGRAMMING Monday 8th July 2024, Tallinn, Estonia A satellite workshop of FSCD 2024 https://msfp-workshop.github.io/msfp2024/ ** Deadline: Tuesday 30th April ** 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: ================ 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, US (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 at umn.edu) and Jeremy Gibbons (jeremy.gibbons at 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 -------------- next part -------------- An HTML attachment was scrubbed... URL: From robby at racket-lang.org Fri Apr 26 21:06:50 2024 From: robby at racket-lang.org (Robby Findler) Date: Fri, 26 Apr 2024 14:06:50 -0500 Subject: [Agda] performance debugging? In-Reply-To: <8452a6c3-c27d-4ea7-b5ad-2f259fe990ed@cse.gu.se> References: <6caeca26-377c-6704-e253-2003e8c7babd@cse.gu.se> <8452a6c3-c27d-4ea7-b5ad-2f259fe990ed@cse.gu.se> Message-ID: On Fri, Apr 26, 2024 at 4:05?AM Nils Anders Danielsson wrote: > I've recently optimised > code with similar characteristics. Perhaps you can do something similar: > > * Prove suitable inversion lemmas for one of the two types. > > * Instead of matching on both arguments, match on one, and use inversion > lemmas for the other argument. > > Wow! That made a huge difference, thank you! That technique took me from 7.5 minutes down to 12 seconds (plus another 2 seconds to check the file with all the inversion lemmas)! That's more than a 35x speed up. Amazing! Also it turns out, I didn't have 2 connected arguments, it was actually 3. (One is an evaluation context and the other two are proofs of decompositions, so the case split on the two decompositions was replaced by the inversion lemmas.) And now that I get the idea, I'm seeing opportunities for this in more places, in this codebase too (not that anything was that slow)! Thanks again! Robby -------------- next part -------------- An HTML attachment was scrubbed... URL: