January 2025 - Haskell-Cafe

Formal Verification & Modern AI Safety
by Mostafa Touny 10 Jan '25

10 Jan '25

Hello Haskellers, I hope you are doing well. Amazon started to adopt automated theorem provers, to mitigate modern Generative AI hallucination. See "Prevent factual errors from LLM hallucinations with mathematically sound Automated Reasoning checks": https://aws.amazon.com/blogs/aws/prevent-factual-errors-from-llm-hallucinat… This community has ties to formal proofs, type-driven programming, and Logic programming. Do you see any special potential of Haskell for recent AI safety? Sincerely, Mostafa Touny

3 2

[ANN] Darcs 2.18.4 release
by Ben Franksen 09 Jan '25

09 Jan '25

Hello Everyone On behalf of the Darcs [1] team, I would like to announce the release of Darcs 2.18.4 [2]. See [3] for the full release notes. The main reason for this release was to make it build with stack against stackage lts-22.34 on Linux. This in turn should hopefully make it re-appear in the Debian and Ubuntu GNU/Linux distros. Cheers Ben [1] https://darcs.net [2] https://hackage.haskell.org/package/darcs-2.18.4 [3] https://hackage.haskell.org/package/darcs-2.18.4/changelog

1 1

Final call for participation: LMS/BCS-FACS Online Seminar, Annabelle McIver, 15 January 2025
by Andrei Popescu 09 Jan '25

09 Jan '25

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(a)lms.ac.uk.

1 0

Rebuilding package on hackage to generate documentation
by Ivan Perez 08 Jan '25

08 Jan '25

Hi, I'm trying to trigger a re-build of Yampa on hackage so that the documentation will be generated. I'm being met with the following message: Report not found Build report does not exist Am I doing something wrong? Thanks Ivan

1 0

[ANN] Copilot 4.2
by Ivan Perez 08 Jan '25

08 Jan '25

Hi everyone!! We are really excited to announce Copilot 4.2 [1,2]. Copilot is a stream-based EDSL in Haskell for writing and monitoring embedded C programs, with an emphasis on correctness and hard realtime requirements. Copilot is typically used as a high-level runtime verification framework, and supports temporal logic (LTL, PTLTL and MTL), clocks and voting algorithms. Compilation to Bluespec, to target FPGAs, is also supported. Copilot is NASA Class D open-source software, and is being used at NASA in drone test flights. Through the NASA tool Ogma [3] (also written in Haskell), Copilot also serves as a runtime monitoring backend for NASA's Core Flight System, Robot Operating System (ROS2), FPrime (the software framework used in the Mars Helicopter). This release introduces several big improvements to Copilot: - Specifications can now use the same handler for multiple monitors, provided that the arguments to those handlers always have consistent types and arity. This simplifies the code that uses Copilot, since it's no longer necessary to create multiple boilerplate wrappers around the same handling routines. - The use of structs has been vastly simplified. Before, it was necessary to define class instances for structs, whose implementations were, although repetitive, not intuitive especially for users unfamiliar with Haskell. In Copilot 4.2, it is now possible to define those methods automatically by relying on default method implementations that work well for most cases, although users retain the ability to customize those methods if desired. - We have increased test coverage in `copilot-core`, reaching full coverage of all elements of the public interface that are not automatically generated by GHC. The interface of `copilot-core` has also been simplified, deprecating record fields of an existential type UExpr, which were largely unused outside of Copilot's internals. The new implementation is compatible with versions of GHC from 8.6 to 9.10, as well as Stackage Nightly. This release has been made possible thanks to key submissions from Frank Dedden, Ryan Scott, and Kyle Beech, the last of which is also a first-time contributor to the project. We are grateful to them for their timely contributions, especially during the holidays, and for making Copilot better every day. We also want to thank the attendees of Zurihac 2024 for technical discussions that helped find the right solutions to some of the problems addressed by this release. For details on this release, see [1]. https://github.com/Copilot-Language/copilot/releases/tag/v4.2. As always, we're releasing exactly 2 months since the last release. Our next release is scheduled for Mar 7th, 2025. We want to remind the community that Copilot is now accepting code contributions from external participants again. Please see the discussions and the issues in our github repo [4] to learn how to participate. Current emphasis is on improving the codebase in terms of performance, stability and test coverage, removing unnecessary dependencies, hiding internal definitions, formatting the code to meet our new coding standards, and simplifying the Copilot interface. Users are encouraged to participate by opening issues, asking questions, extending the implementation, and sending bug fixes. Happy Haskelling! Ivan -- [1] https://github.com/Copilot-Language/copilot/releases/tag/v4.2 [2] https://hackage.haskell.org/package/copilot [3] https://github.com/nasa/ogma [4] https://github.com/Copilot-Language/copilot

1 0

POPL 2025 Call for Participation (January 19-25, Denver, Colorado)
by Ningning Xie 07 Jan '25

07 Jan '25

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

1 0

CGO'25 - early bird registration and student research competition
by Luisa Cicolini 07 Jan '25

07 Jan '25

Dear all, Registrations for the International Symposium on Code Generation and Optimization (CGO) 2025<https://2025.cgo.org/>, taking place in Las Vegas<https://2025.cgo.org/attending/Venue>, from 1st-5th March are now open. The International Symposium on Code Generation and Optimization (CGO) is a premier venue bringing together researchers and practitioners working at the interface of hardware and software on a wide range of optimization and code generation techniques and related issues. The conference spans from purely static to fully dynamic approaches, from pure software-based methods to specific architectural features and support for code generation and optimization. Early registration<https://2025.cgo.org/attending/registration> deadline is on 31st January! We are also hosting a Student Research Competition (SRC)<https://2025.cgo.org/track/cgo-2025-student-research-competition>: a unique opportunity for undergraduate and graduate students to present their original research before a panel of judges and attendees at CGO'25. The winner will be awarded and invited to the 2025 ACM SRC competition. If you know any undergraduate or postgraduate students doing research in compiler-related topics, please invite them to apply - we are excited to welcome young researchers to the community! Best, Luisa Cicolini

1 0