Canberra2024
IFIP 2.1 Meeting #82 Information
The 82nd meeting will be organised by Peter Höfner and Carroll Morgan.
Location: Canberra, Australia.
Dates
Monday November 25, 2024 to Friday November 29, 2024.
(Meeting starts at 8:50am on that Monday morning.)
Participants
| Name | Function |
|---|---|
| Alberto Pardo | member |
| Azalea Raad | observer |
| Carroll Morgan | organiser |
| Donovan Crichton | local observer |
| Farzaneh Derakhshan | observer |
| Janis Voigtländer | member |
| Lambert Meertens | member |
| Liam O'Connor | observer |
| Nick Wu | member |
| Bruno Oliveira | member |
| Peter Höfner | chair, organiser |
| Sam Lindley | member |
| Thomas Sewell | local observer |
| Tom Schrijvers | secretary |
| Walter Guttmann | member |
| Youyou Cong | observer |
Practical information
Consult the separate “practical” page for more detailed information: precise location, budget, travel advice etc.
Organizational and administrative matters
Friday morning, November 29, 2024.
Membership
These private matters are not recorded in the public version of the minutes.
Formal resolution
The members and observers of IFIP WG2.1 were drawn as flies to Meeting #82 in the honeypot that is Canberra. While chasing the elusive bettong along Lambert's songline, avoiding the vicious drop bear and sav(or)ing (the aroma of) half a dozen long neck turtles, they resolve to heed the seven wisdoms of the swooping magpies:
- One for sorrow...........................Remembering our dear friend and colleague Cezar
- Two for joy..............................Welcoming outstanding new observers
- Three for a girl.........................Typecasting Eve no more
- Four for a boy...........................Wanting to be the adversary sometimes too
- Five for silver..........................Knowing the cost of all things, and the value of some things
- Six for gold.............................Perferring it much over Amber
- Seven for a secret never to be told......Using a noninterfering protocol.
They acknowledge and celebrate the First Australians on whose traditional lands they met, and pay their respect to the elders past and present. Above all, they are grateful to Peter Hoefner, Carroll Morgan and Donovan Crichton for organizing this most upside down meeting.
Next meetings:
- M83 (Sep 2025) Portugal.
- M84 (May 2026) Estonia.
- M85 (Feb 2027) To be determined.
Technical presentations in scheduled order
Lambert Meertens, Using affix grammars to compose music (Monday, November 25 2024, 10:31 -- 11:39)
IFIP held a computer-composed music competition in connection with IFIP Congress 68. I submitted a string quartet that received a special mention from the jury. The program that generated the score for the string quartet was based on an affix grammar, a two-level grammar formalism that I had invented earlier to generate natural-language text.
Sam Lindley, Modal effect types (Monday, November 25 2024, 11:42 -- 12:42)
Effect handlers are a powerful abstraction for defining, customising, and composing computational effects. Statically ensuring that all effect operations are handled requires some form of effect system, but using a traditional effect system would require adding extensive effect annotations to the millions of lines of existing code in these languages. Recent proposals seek to address this problem by removing the need for explicit effect polymorphism. However, they typically rely on fragile syntactic mechanisms or on introducing a separate notion of second-class function. We introduce a novel semantic approach based on modal effect types.
Youyou Cong, Teaching continuations to the rest of us (Monday, November 25 2024, 14:00 -- 14:43)
In this talk, I share my experience teaching continuations in a graduate course. Specifically, I present a programming language designed for learners of continuations, and report the results of three experiments conducted in the course.
Liam O'Connor, Holbert: Reading, writing and proving in the browser (Monday, November 25 2024, 14:45 -- 15:50)
Holbert is a graphical proof assistant and document preparation system for making tool-supported textbooks in the vein of Software Foundations or Concrete Semantics, but without the heavy overhead of full-blown proof assistants. Visually, proofs are constructed interactively and the resultant proof artefact is a hopefully-readable document using notation broadly similar to the common Computer Science Meta Notation (to borrow a phrase from Guy Steele) to which many of us are accustomed.
Nicolas Wu, Modular Effective Programming (Monday, November 25 2024, 16:13 -- 17:02)
This talk outlines the use of a library for programming with higher-order effects.
Azalea Raad, Incorrectness logic for bug detection (Tuesday, November 26 2024, 9:05 -- 10:08)
Incorrectness Logic (IL) has recently been advanced as a logical under-approximate theory for proving the presence of bugs - dual to Hoare Logic, which is an over-approximate theory for proving the absence of bugs. To facilitate scalable bug detection, later we developed incorrectness separation logic (ISL) by marrying the under-approximate reasoning of IL with the local reasoning of separation logic and its frame rule. This locality leads to techniques that are compositional both in code (concentrating on a program component) and in the resources accessed (spatial locality), without tracking the entire global state or the global program within which a component sits. This enables reasoning to scale to large teams and codebases: reasoning can be done even when a global program is not present. This led to the development of Pulse-X, an automatic program analysis for catching memory safety errors, underpinned by ISL and subsequently deployed at Meta.
Tom Schrijvers, Simulating {Nondeterminism and State} with State (Tuesday, November 26 2024, 10:45 -- 11:35)
Some effects are considered to be higher-level than others. High-level effects provide expressive and succinct abstraction of programming concepts, while low-level effects allow more fine-grained control over program execution and resources. Yet, often it is desirable to write programs using the convenient abstraction offered by high-level effects, and meanwhile still benefit from the optimizations enabled by low-level effects. One solution is to translate high-level effects to low-level ones.
This paper studies how algebraic effects and handlers allow us to simulate high-level effects in terms of low-level effects. In particular, we focus on the interaction between state and nondeterminism known as the local state, as provided by Prolog. We map this high-level semantics in successive steps onto a low-level composite state effect, similar to that managed by Prolog's Warren Abstract Machine. We first give a translation from the high-level local-state semantics to the low-level global-state semantics, by explicitly restoring state updates on backtracking. Next, we eliminate nondeterminism altogether in favor of a lower-level state containing a choicepoint stack. Then we avoid copying the state by restricting ourselves to incremental, reversible state updates. We show how these updates can be stored on a trail stack with another state effect. We prove the correctness of all our steps using program calculation where the fusion laws of effect handlers play a central role.
Carroll Morgan, Programming for reasoning quantitatively about leaks and adversaries at the source level (Tuesday, November 26 2024, 11:39 -- 12:27)
A source-level logic for reasoning about quantitative information flow is presented, together with some small examples that illustrate how it might work. The context is "Kuifje", whose denotational (monad-based) semantics has been worked out some time ago. But the "post-gain -to- greatest pre-gain" logic (analogous to "postcondition to weakest pre-condition") is new this year.
Bruno Oliveira, QuickSub: Efficient Iso-Recursive Subtyping (Tuesday, November 26 2024, 14:15 -- 15:22)
Many programming languages need to check whether two recursive types are in a subtyping relation. In this talk we present QuickSub: an efficient and simple to implement algorithm for iso-recursive subtyping. QuickSub has the same expressive power as the well-known iso-recursive Amber rules. The worst case complexity of QuickSub is O(nm), where m is the size of the type and n is the number of recursive binders. However, in practice, the algorithm is nearly linear with the worst case being hard to reach. Consequently, in many common cases, QuickSub can be several times faster than alternative algorithms. We validate the efficiency of QuickSub with an empirical evaluation comparing it to existing equi-recursive and iso-recursive subtyping algorithms.
Farzaneh Derakhshan, Modal crash types for intermittent computing (Tuesday, November 26 2024, 15:51 -- 16:53)
Intermittent systems face arbitrary power failures, resulting in programs being executed intermittently. To ensure progress, these systems need runtime support to checkpoint state and re-execute after power failure by restoring the last saved state. Such re-execution should be correct, i.e., simulated by a continuously-powered execution. In this presentation, we focus on the logical underpinning of intermittent computing and model the checkpoint, crash, restore, and re-execution operations as computation on Crash types. Inspired by adjoint logic, we define Crash types using two modality operators that distinguish between persistent and transient memory states, and model the transitions between them caused by checkpoints and restoration. We prove the correctness of intermittent systems by designing a logical relation for Crash types.
Walter Guttmann, Kleene Algebra of Convex Polygons (Wednesday, November 27 2024,9:05 -- 10:02)
Languages and binary relations form well-known Kleene algebras, which describe choice, sequence and iteration. A less well-studied model proposed by Iwano and Steiglitz are convex polygons. We show how this geometrical model arises from closure operators over groups, the corresponding closure systems, and convex spaces. We also obtain the geometrical model using intersections of convex-closed sets in partial orders.
Thomas Sewell, Dividing a Big-Step Semantics (Wednesday, November 27 2024,10:07 -- 11:01)
In this talk, I give an overview of one aspect of the seL4 verification that I would like to change. The traces by which system execution is modelled are generated by a simple automaton in which the kernel's execution is private and terminates. The sytem call handlers also exit as C functions, so the traces can be understood from the big-step semantics of the C program. This makes the verification problem easy to phrase.
To verify a user-level task, however, we would like to rephrase this characterising automaton to agree with the perspective of that task. I argue that this might be accomplished by subdividing the kernel steps, breaking up its big steps.
Janis Voigtlaender, Exercise Task Generation for a Modelling Course Using Alloy (Thursday, November 28 2024,9:08 -- 10:18)
We discuss the usage of Alloy for generating correct-by-construction exercise tasks for a course covering various diagrammatic model languages. One interesting aspect of the development is the varying degree to which the specifications can reuse features of the Alloy language itself.
Alberto Pardo, Packrat-parsing Tabulation Technique (Thursday, November 28 2024,14:01 -- 15:02)
abstract
Farzaneh Derakhshan, Noninterference for session typed processes (Thursday, November 28 2024, 15:05 -- 15:50)
In this talk, I present our prior work on the development of an information flow control system for linear binary session types. I also discuss extending the work to include quantitative analysis in the type system.
Liam O'Connor, I don't have all day: Examining linear-time temporal {Properties, Logic} within finite time (Friday, November 29 2024, 11:34 -- 12:16)
We define a proper inductive semantics for LTL which includes those finite partial traces for which a definitive answer can be given: the “definitive prefixes” of the property. Sets of definitive prefixes are called definitive sets. Defining a semantics for LTL in terms of definitive sets gives us something equivalent to LTL3, a formulation popular in runtime verification. Our theory of definitive sets is sufficient to give a neat characterisation of (co-)safety and (co-)liveness properties, allowing us to straightforwardly prove Alpern and Schneider’s result that every property is the intersection of a safety and liveness property by simpler means.
Problem-Solving Sessions
TBD
Schedule
Sessions will start at 9:00 on Monday and finish at noon on Friday. There will be an excurion mid-week, and a workshop dinner.
