Hi everyone!!
We are very excited to announce Copilot 3.17 [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.
Copilotis being used at NASA in drone test flights. Through the NASA tool
Ogma [1] (also written in Haskell), Copilot also serves as a runtime
monitoring backend for NASA's Core Flight System, Robot Operating System
(ROS2), and FPrime (the software framework used in the Mars Helicopter)
applications.
This release introduces compatibility with what4 versions up to 1.5.1, and
replaces several functions in copilot-core. The second change is a breaking
change: the functions replaced have been deprecated and new alternatives
introduced instead.
As always, we're releasing exactly 2 months since the last release. Our
next release is scheduled for Jan 7th, 2024.
In our last announcement, we mentioned that Copilot has received full
approval for release as NASA Class D open-source software. Current emphasis
is on increasing test coverage for the two remaining libraries without
tests (copilot-libraries and copilot-theorem), removing unnecessary
dependencies, hiding internal definitions, and formatting the code to meet
our new coding standards. Users are encouraged to participate by opening
issues and asking questions via our github repo [3].
There have been many updates on the Copilot front in the last few months.
We'll be able to announce more soon. Stay tuned. Happy Haskelling!
Ivan
[1] https://github.com/nasa/ogma
[2] https://github.com/Copilot-Language/copilot/releases/tag/v3.17
[3] https://github.com/Copilot-Language/copilot
[4] https://hackage.haskell.org/package/copilot
========================================================================
BOB Conference 2024
"What happens when we use what's best for a change?"
https://bobkonf.de/2024/cfc.html
Berlin, Mar 17
Call for Contributions
Deadline: November 17, 2023
========================================================================
You are actively engaged in advanced software engineering methods,
solve ambitious problem with software and are open to cutting-edge
innovation? Attend this conference, meet people that share your goals,
and get to know the best software tools and technologies available
today. We strive to offer a day full of new experiences and
impressions that you can use to immediately improve your daily life as
a software developer.
If you share our vision and want to contribute, submit a proposal for
a talk or tutorial!
NOTE: The conference fee will be waived for presenters. Travel
expenses will not be covered (for exceptions see "Speaker Grants").
Shepherding
-----------
The program committee offers shepherding to all speakers. Shepherding
provides speakers assistance with preparing their
sessions. Specifically:
- advice on structure and presentation
- review of talk slides
Speaker Grants
--------------
BOB has Speaker Grants available to support speakers from groups
under-represented in technology. We specifically seek women speakers,
speakers of color, and speakers who are not able to attend the
conference for financial reasons.
Topics
------
We are looking for talks about best-of-breed software technology, e.g.:
- functional programming
- persistent data structures and databases
- event-based modelling and architecture
- "fancy types" (dependent types, gradual typing, linear types, ...)
- formal methods for correctness and robustness
- abstractions for concurrency and parallelism
- metaprogramming
- probabilistic programming
- math and programming
- controlled side effects
- program synthesis
- next-generation IDEs
- effective abstractions for data analytics
- … everything really that isn’t mainstream, but you think should be
- … includeing rough ideas worth discussing.
Presenters should provide the audience with information that is
practically useful for software developers.
Challenges
----------
Furthermore, we seek contributions on successful approaches for
solving hard problems, for example:
- bias in machine-learning systems
- digital transformation in difficult settings
- accessibiltity
- systems with critical reliability requirements
- ecologically sustainable software development
We're especially interested in experience reports.
Other topics are also relevant, e.g.:
- introductory talks on technical background
- overviews of a given field
- demos and how-tos
Requirements
------------
We accept proposals for presentations of 45 minutes (40 minutes talk +
5 minutes questions), as well as 90 minute tutorials for
beginners. The language of presentation should be either English or
German.
Your proposal should include (in your presentation language of choice):
- An abstract of max. 1500 characters.
- A short bio/cv
- Contact information (including at least email address)
- A list of 3-5 concrete ideas of how your work can be applied in a
developer's daily life
- additional material (websites, blogs, slides, videos of past presentations, …)
Organisation
------------
- Direct questions to konferenz at bobkonf dot de
- Proposal deadline: November 17, 2023
- Notification: December 5, 2023
- Program: December 12, 2023
Submit here:
https://pretalx.com/bob-2024/submit/
Program Committee
-----------------
(more information here: https://bobkonf.de/2024/programmkomitee.html)
- Matthias Fischmann, Wire
- Matthias Neubauer, SICK AG
- Nicole Rauch, Softwareentwicklung und Entwicklungscoaching
- Michael Sperber, Active Group
- Stefan Wehr, Hochschule Offenburg
Scientific Advisory Board
- Annette Bieniusa, TU Kaiserslautern
- Torsten Grust, Uni Tübingen
- Peter Thiemann, Uni Freiburg
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512
According to the Haskell report [1] (See Note 5), a virtual `}` token
is inserted if parsing the next token would cause a parse error and the
indentation stack is non-empty.
I'm trying to lex and parse Haskell source and this sort of interplay
(which requires two-way communication between lexer and parser) makes
it very difficult to write a conformant implementation.
I can't change the standard (obviously), but I'm wondering if this is
actually what GHC (de facto the only Haskell compiler) does, or if it
applies some other rule. If so, does anyone know the exact mechanism of
its implementation?
I've been programming Haskell for more than a decade, and while I have
an intuitive understanding of the indentation rules, I would have
assumed the source could be lexed without also having a parser. In
particular, the note seems to imply that the main purpose of this is to
properly lex `let`/`in` bindings. Perhaps there's an alternate
equivalent rule?
Curious to hear other's thoughts.
Travis
[1]
https://www.haskell.org/onlinereport/haskell2010/haskellch10.html#x17-17800…
-----BEGIN PGP SIGNATURE-----
iIsEARYKADMWIQRW81c55hOCXuY5k/H+BxaRGQDTjQUCZUGARhUcdHJhdmlzQGF0
aG91Z2llcy5uZXQACgkQ/gcWkRkA041W+wEA/7n5NejGTYu4O6N+Pt7Rn0bBRw6D
5D96idagahXqXioA/18hxYFpY45lWwB7pKCh83xQJu2Bcwkxj1xhhCEZBcoA
=FrDy
-----END PGP SIGNATURE-----
