From matthewdaggitt at gmail.com Fri Jan 3 10:20:30 2025 From: matthewdaggitt at gmail.com (Matthew Daggitt) Date: Fri, 3 Jan 2025 17:20:30 +0800 Subject: [Agda] [ANNOUNCE] Agda Standard Library Version 2.2 - Release Candidate 1 Message-ID: Dear all, The Agda Team is pleased to announce the first release candidate for version 2.2 of the Agda standard library. The release candidate has been tested using Agda 2.7.0 and 2.7.0.1 and can be downloaded here . The CHANGELOG is available here . We would be grateful for reports of any issues you may encounter with the new version of the library on the Github issues page . If there are no further issues found, we plan to make the official release next week. Best wishes, Matthew, on behalf of the Agda Team -------------- next part -------------- An HTML attachment was scrubbed... URL: From xnningxie at gmail.com Tue Jan 7 17:21:48 2025 From: xnningxie at gmail.com (Ningning Xie) Date: Tue, 7 Jan 2025 11:21:48 -0500 Subject: [Agda] POPL 2025 Call for Participation (January 19-25, Denver, Colorado) Message-ID: The 52nd ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2025) will take place in January in Denver, Colorado, the United States. It's going to be an amazing conference - don't miss it - sign up now! https://popl25.sigplan.org/attending/registration Location: Curtis Hotel Denver, 1405 Curtis Street, 80202, Denver, Colorado, United States Dates: - Main conference: Wed 22 - Fri 24 January - Workshops, tutorials, co-located events: Sun 19, Mon 20, Tue 21 and Sat 25 January Accepted papers: https://popl25.sigplan.org/track/POPL-2025-popl-research-papers Full details of the conference and co-located events: https://popl25.sigplan.org/ Sponsors: POPL is supported by generous sponsorship from: - Amazon - Jane Street - Google DeepMind - JetBrains - Microsoft - Epic - Google - Ahrefs -------------- next part -------------- An HTML attachment was scrubbed... URL: From andrei.h.popescu at gmail.com Thu Jan 9 02:21:20 2025 From: andrei.h.popescu at gmail.com (Andrei Popescu) Date: Thu, 9 Jan 2025 01:21:20 +0000 Subject: [Agda] Final call for participation: LMS/BCS-FACS Online Seminar, Annabelle McIver, 15 January 2025 Message-ID: LMS/BCS-FACS Seminar 2025 Wednesday 15 January 2025, from 19:00 (GMT) Online via Zoom https://www.lms.ac.uk/events/lms-bcs-facs-seminar-2025 In association with the British Computer Society Formal Aspects of Computing Science (BCS-FACS), the LMS hosts an annual online seminar on aspects of the computer science?mathematics interface. These events are free to anyone who wishes to attend and have attracted high-quality speakers. We are happy to have this verification talk from a wonderful speaker just one day after World Logic Day. Speaker: Annabelle McIver (Macquarie University) Probabilistic Datatypes: automating verification for abstract probabilistic reasoning Abstract: Datatypes - in which data is encapsulated together with methods that access it - play an important role in the organisation of large software projects. Correctness of datatypes has traditionally been carried out using simulation relations to simplify the verification by separating concerns: the datatype can be verified independently from the programs that use it, whilst those programs themselves can be verified using the specifications of the datatype's methods. Use of these principles enables complex programs to be brought within reach of automated proof. When probabilistic choice is included, however, it turns out that obtaining similar simplifications of the verification problem will require distinguishing between "hidden" and "observable" probabilistic behaviour - if demonic choice is allowed in the surrounding program. And that is not required in the non-probabilistic setting: the crucial issue is the potential interaction of probabilistic- and demonic choice. In the main part of this talk I will use examples to explain why the interaction is problematic, and I will suggest how extension of existing pGCL-based automated reasoning-tools, will by taking that interaction into account, enable automated probabilistic abstract reasoning about "hard to crack" probabilistic programs. Registration: To attend remotely via Zoom, please complete the registration form here: https://www.lms.ac.uk/civicrm/event/info?reset=1&id=139 You will receive the link to the meeting upon registration, as well as an automated reminder email sent 24 hours before the event is scheduled to start. For all queries regarding the seminar, please contact lmscomputerscience at lms.ac.uk. -------------- next part -------------- An HTML attachment was scrubbed... URL: From matthewdaggitt at gmail.com Wed Jan 15 02:58:36 2025 From: matthewdaggitt at gmail.com (Matthew Daggitt) Date: Wed, 15 Jan 2025 09:58:36 +0800 Subject: [Agda] [ANNOUNCE] Agda Standard Library Version 2.2 Message-ID: Dear all, The Agda Team is pleased to announce the release of version 2.2 of the Agda standard library. The release has been tested using Agda 2.7.0 and 2.7.0.1 and can be downloaded here . The CHANGELOG is available here . Best wishes, Matthew, on behalf of the Agda Team -------------- next part -------------- An HTML attachment was scrubbed... URL: From felix.wellen at posteo.de Wed Jan 15 20:03:43 2025 From: felix.wellen at posteo.de (Felix Wellen) Date: Wed, 15 Jan 2025 19:03:43 +0000 Subject: [Agda] Final CfP for HoTT/UF 2025 Message-ID: ========================================================== FINAL CALL FOR CONTRIBUTIONS AND PARTICIPATION Workshop on Homotopy Type Theory and Univalent Foundations (HoTT/UF 2025, co-located with WG6 meeting of the EuroProofNet COST action) ========================================================== ------------------------------------------------------------------------ Workshop on Homotopy Type Theory and Univalent Foundations 15?16 April 2025, Genoa, Italy https://hott-uf.github.io/2025/ Co-located with the WG6 meeting of the EuroProofNet COST action 17?18 April 2025 https://europroofnet.github.io/wg6-genoa/ ------------------------------------------------------------------------ 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 * Reid Barton (Carnegie Mellon University, USA) * Bastiaan Cnossen (University of Regensburg, Germany) * Ambrus Kaposi (E?tv?s Lor?nd University, Hungary) ================ # Submissions * Abstract submission deadline: 7 February 2025 * Author notification: 10 March 2025 Submissions should consist of a title and an abstract of no more than 2 pages (not counting the list of references) in pdf format, via https://easychair.org/conferences/?conf=hottuf2025. 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 for HoTT/UF is mandatory with a deadline of 28 March 2025 (AoE). Registration information will be provided shortly. *If you require funding, we encourage you to apply to EuroProofNet via the WG6 registration before the deadline of 4 March 2025*. There is no need to await the HoTT/UF author notification. ================ # Program committee * Ulrik Buchholtz (University of Nottingham) * Pierre Cagne (Applachian State University) * Dan Christensen (The University of Western Ontario) * Felix Cherubini (Chalmers University of Technology/University of Gothenburg) * Tom de Jong (University of Nottingham) * Jonas Frey (Universit? Sorbonne Paris Nord) * Daniel Gratzer (Aarhus University) * Philipp Haselwarter (Aarhus University) * Andr?s Kov?cs (University of Gothenburg) * Anja Petkovi? Komel (TU Wien) * Lo?c Pujet (University of Stockholm) * Mitchell Riley (NYU Abu Dhabi) ================ # Organizers * Felix Cherubini, felix.cherubini at posteo.de (Chalmers University of Technology/University of Gothenburg) * Tom de Jong, tom.dejong at nottingham.ac.uk (University of Nottingham) * Daniel Gratzer, gratzer at cs.au.dk (Aarhus University) * Mitchell Riley, mitchell.v.riley at nyu.edu (NYU Abu Dhabi) From matthewdaggitt at gmail.com Thu Jan 16 01:58:25 2025 From: matthewdaggitt at gmail.com (Matthew Daggitt) Date: Thu, 16 Jan 2025 08:58:25 +0800 Subject: [Agda] [ANNOUNCE] Agda Standard Library Version 2.2 In-Reply-To: <81dd2f7b78c4b0284e07aceb791501e1@scico.botik.ru> References: <81dd2f7b78c4b0284e07aceb791501e1@scico.botik.ru> Message-ID: Apologies, it has been pointed out that the links in the previous email accidentally pointed to the 1st release candidate and not the official release. The corrected links are below: > The Agda Team is pleased to announce the release of version 2.2 of the Agda standard library. The release has been tested using Agda 2.7.0 and 2.7.0.1 and can be downloaded here . The CHANGELOG is available here . Best wishes, Matthew, on behalf of the Agda Team On Thu, Jan 16, 2025 at 3:37?AM wrote: > On 2025-01-15 04:58, Matthew Daggitt wrote: > > Dear all, > > > > The Agda Team is pleased to announce the release of version 2.2 of the > > Agda standard library. The release has been tested using Agda 2.7.0 > > and 2.7.0.1 and can be downloaded here [1]. The CHANGELOG is available > > here [2]. > > Setting the pointer at "here" shows the URL ".../v2.2-rc1", > but clicking at it downloads the file that has name "...2.2.zip". > I doubt a bit about what people would think about the name > ".../v2.2-rc1". > > Regards, > > ------ > Sergei > -------------- next part -------------- An HTML attachment was scrubbed... URL: