You are here: Foswiki>IFIP21 Web>Taiwan (05 Apr 2019, ConorMcBride)Edit Attach

Meeting Information

The 78th meeting will be organised by Shin-Cheng Mu.

Location: Taiwan.

For practical information, go to Taiwan (practical).


Monday 2019-03-18 to Friday 2019-03-22. (Meeting starts on Monday morning.)


Name Function
Tom Schrijvers secretary
Carroll Morgan chair
Shin-Cheng Mu organizer
Jeremy Gibbons  
Lambert Meertens  
Florian Rabe  
Fritz Henglein  
Johan Jeuring  
Janis Voigtländer  
Brijesh Dongol Observer
Bruno Oliveira  
Graham Hutton  
Oleg Kiselyov  
Patrik Jansson  
Pierre-Evariste Dagand Observer
Brent Yorgey Observer
Bernhard Möller  
Kazutaka Matsuda Observer
Hsiang-Shang (Josh) Ko Observer
James McKinna  
Doaitse Swierstra  
Sam Lindley Observer
José Pedro Magalhães  
Ralf Hinze  
Sergio Antoy Observer
Tarmo Uustalu  
Conor McBride  
Marcos Viera Observer
Ting-Yan Lai Local Observer
See also the table of participants on the “practical” page for detailed practical information

Organizational and administrative matters

Friday morning, March 22, 2019.
These private matters are not recorded in the public version of the minutes.
Formal resolution
The members and observers of IFIP WG2.1 present at Meeting #78 in Xitou in Taiwan would like to thank Shin-Cheng Mu for organising the meeting and for choosing such an excellent venue.

We thank also his assistants Kai-Jan Han, Shao-Chuan (Winnie) Chang and Ting-Yan Lai for making the meeting run so smoothly.

And we are grateful to Bow-Yaw Wang and Tyng-Ruey Chuang for helping to secure financial support from the Institute of Information Science, Academia Sinica.


Indeed we were very eager to come to Taiwan:

"After listening to many scholars, we learned what they taught and understood the meanings in detail; but they were specialising within their topics, and straying from rigorous calculational principles.

"We couldn't know what was right. That's why we vowed to go to Xitou and solve the confusions."

[adapted from Xuan Zang]

Unlike Xuan Zang, who encountered "barren deserts, devoid of living animals, humans and plants, with skeletons everywhere" we found a beautiful verdant wilderness, with food in superabundance; and there were plenty of humans to be seen. Further, living animals abounded, many of whose (very) early-morning twitterings were exactly the same as one's wake-up alarm on the iPhone --- an admirable economy when one is dealing with jet-lag.

There was however a skeleton of a giant tree.

Next meetings:
  • M79 (Dec 2019/Jan 2020) Veluwe (NL).
  • M80 (Aug 2020) Germany?

Scheduling of talks for the Taiwan meeting

As usual, in the very first session people will introduce themselves, stating whether they want to give a talk (but no more details about the talk than that). And then we will have the short "advertising" talks.

Short talks

The short talks will however be longer than in the recent past, their time limit adjusted uniformly so that they will finish by the mid-afternoon break, minus ten minutes or so for voting. (That is later than usual; given the potential Taiwan numbers, that could be about 10 minutes for each.) As the talks are given, we'll collect titles, ready-by-when and expected length as usual, with the last being an estimate without questions.

If you want to use a projector for your short talk, please upload/send your material to the Secretary before he leaves (Belgium) for the meeting, so that he can arrange to have them on his laptop when the meeting starts. That will avoid the usual messing about with cables etc. (Please email the Secretary if you have questions about how to upload, or what hardware/software the laptop for the short talks will support.)

You do not have to use a projector for your short talk, of course; nor do you need to take the full time (however many minutes it turns out to be).

Full talks

The time estimate for your full talk is not taken as a guarantee of any kind (for example that you will get at least that time, or no more than that time) — it is just to help people decide how to vote.

During the afternoon break the first few full talks will be scheduled, that is for the final session (2 hours) on Monday.

Observers' talks will be scheduled (put at the head of the queue) for first thing Tuesday, and so all observers who want to talk __should be ready to do so right from the beginning__. Other talks will be ordered at the officers' discretion, that is to say not necessarily in terms of popularity. (We might want to group topics etc.)

The full talks themselves will not have a fixed time-limit, in particular not the time that the speaker advertised. Instead, the Chairman will decide at some point to ask the audience whether the talk should continue, or be finished up (depending on the interest that the talk has evoked). A show of hands will help to determine the outcome; and that could happen several times for a single talk.

The Chairman will try to keep questions more or less on topic (intervening if necessary). But there will be no coloured cards and no chess clock.


The main effects of the above are intended to be: (1) the longer short-talks will give people a better idea of what full talks they are voting for; (2) everyone will get to speak for (nominally) 10 minutes at least, if they wish; and (3) participants must not have the expectation that their full talk will necessarily be scheduled --- if earlier talks turn out to be of great interest to a significant part of the group, later talks will indeed never be reached.

During the members' meeting we will discuss how it went, and what we should settle on for the medium-term future. In the meantime (for example during the excursion) people are encouraged to discuss it, since by then people will have seen how it is working.

Please email the chairman directly if you have questions.

Short presentation

Jeremy Gibbons, The Genuine Sieve of Eratosthenes
Chapter 9 of Richard Bird's book Thinking Functionally with Haskell presents a very nice circular program for computing all the primes, and sets as an exercise the proof of its correctness, with a proof sketch as the solution to the exercise. The proof sketch is simply wrong. In fact, I can't immediately complete the proof myself. I'd like to work out what the proof should be, and then what the errata for the book should say as a hint.


Technical presentations in scheduled order

Brijesh Dongol, Towards a Hoare Logic for C11 (Monday, March 18, 2019, 14:10--15:20)
We present an operational semantics for the release-acquire fragment of the C11 memory model with relaxed accesses. The semantics is both sound and complete with respect to the axiomatic model of Batty et al. We rely on a per-thread notion of observability, which allows one to reason about a weak memory C11 program in program order. On top of this, we build an assertion language and a Hoare-like proof system, which is used to prove correctness of the message-passing litmus test.


Kazutaka Matsuda, Sparcl (Monday, March 18, 2019, 15:55-17:06)
Invertibility is a fundamental concept both in mathematics and computer science, and in software development, invertible computations occur frequently in various forms (serializer/deserializer, parser/printer, redo/undo, compressor/decompressor, and so on). Strict invertibility necessarily requires bijectivity, which is too restrictive for compositional programming in practice. This talk, we focus on partially-invertible computations and presents a language Sparcl for programming them in a natural way. Partially invertible functions are functions that may become invertible if some of their arguments are fixed. The simplest example of such is addition, which becomes invertible when one of the operands is fixed. More involved examples include entropy-based compression methods (e.g., Huffman coding), which carry occurrence frequency of input symbols in some format (e.g., Huffman tree), and the compression methods become invertible after fixing this information. The language Sparcl is based on Wadler [1993]'s linear lambda calculus. The key idea is to distinguish data that are subject to invertible computation and that are not by using types. We design the syntax, type system, and semantics of the language, and prove that Sparcl correctly guarantees invertibility for its programs.


Josh Ko, Streaming Metamorphisms in Agda (Monday, March 18, 2019, 17:09-17:50)
A metamorphism is a fold followed by an unfold, the former consuming a data structure to compute an intermediate value and the latter producing a codata structure from that value. Bird and Gibbons considered streaming metamorphisms on lists, which, under a commutativity condition, can possibly start producing the output without having to consume all the input. In Agda, we can encode a metamorphic specification in a type such that any program with that type correctly implements the metamorphism. In addition, for streaming metamorphisms, type information can help us find out the commutativity condition as we program the streaming algorithm in Agda’s interactive development environment.


Pierre-Evariste Dagand, A Study in Deforestation: Diff-ing (and more) in Xitou (Tuesday, March 19, 2019, 9:01-9:53)
In the literature on string processing, we find several, apparently unrelated, algorithms for computing the longest increasing subsequence (LIS, solved by Robinson & Schensted), heaviest increasing subsequence (HIS, solved by Jacobson & Vo), longest common subsequence (LCS, solved by Hunt-Szymanski) and heaviest common subsequence (HCS, solved by Jacobson-Vo). In this work, we propose a rational reconstruction of all four algorithms thanks to a single, suitably generalized data-structure. Besides, we show how LIS and LCS arise as specialization of HIS and, respectively, HCS. Finally, we touch upon the challenge of improving the algorithmic complexity of our implementation of HCS/LCS.


Brent Yorgey, Disco: A Functional Teaching Language for Discrete Mathematics (Tuesday, March 19, 2019, 9:55-11:31)


Sergio Antoy, Declarative Programming in Curry (Tuesday, March 19, 2019, 11:35-12:15)
Curry is a general-purpose, high-level, functional logic programming language. In Curry, computations are executed by narrowing that promotes the development of non-deterministic algorithms that are closer to specification than to programs. This talk offers a crash introduction of Curry with focus on narrowing, its evaluation strategy, and its application to a set of illustrative examples.


Sam Lindley, Interdefinability of equi- and iso-recursive types (Tuesday, March 19, 2019, 13:50-14:41)

Marcos Viera, MateFun: Functional Programming and Math with Teenagers (Tuesday, March 19, 2019, 14:43-15:38)
In this presentation I introduce the language MateFun, a functional programming language designed to teach mathematics in high-school. We go through the most important design decisions and show some possible future work.


Ralf Hinze, Combles (Tuesday, March 19, 2019, 16:14-16:54)


Jeremy Gibbons, Asymmetric Numeral System (Tuesday, March 19, 2019, 16:56-17:52)
Asymmetric Numeral Systems (ANS) are an entropy-based encoding method introduced by Jarek Duda in 2013, combining the Shannon-optimal coding effectiveness of arithmetic coding with the execution efficiency of Huffman coding. This combination has seen ANS adopted by companies such as Facebook, Apple, Google, and Dropbox. I presented the outline of a derivation of ANS, starting with arithmetic coding (as in lecture notes by Richard Bird and myself from 2002), explaining the key insight by which ANS works, and highlighting the main differences between the two approaches.


Tom Schrijvers, Handling Local State with Global State (Wednesday, March 20, 2019, 9:05-10:00)
This is joint work with Shin-Chen Mu and Koen Pauwels.

We consider the interaction between monadic renditions of the state and non-determinism effects. There are two prominent interactions in the literature: local state semantics and global state semantics. We characterise these with laws and show how to simulate local state semantics using global state semantics.

To prove the correctness of this simulation we reconcile the typical denotational approach to semantics for monads with a syntactic approach to semantics that is convenient for inductive proofs that can be mechanised in a proof assistant. We do this by means of free monads that capture the syntax of effectful programs, but not their semantics. The semantics is obtained by mapping into a semantic domain, and requires us to express the effect laws on the free monad in terms of contextual equivalence.

In order to make the simulation work, we require two non-contextual laws. These laws are not satisfied by conventional monadic models, but thanks to our free monad approach we get the monadic structure for free and can supply a non-monadic model.


José Pedro Magalhães, Insights from a large scale, realistic use of Haskell in production (Wednesday, March 20, 2019, 10:00-11:23)

Carroll Morgan, Quantitative Information Flow and Collateral (Dalenius) Leakage gives a Natural Transformation (Wednesday, March 20, 2019, 11:24-12:00; continued Thursday, March 21, 9:02-9:40)

Oleg Kiselyov, Polynomial Event Semantics: Non-Montagovian Proper Treatment of Quantifiers (Thursday, March 21, 9:42-10:35)
Montagovian semantics and the Montagovian treatment of quantification introduced lambda calculus and the continuation-passing style into natural language semantics. After a brief introduction to Montagovian approach, we outline an alternative. We account for the universal, existential and counting quantification, with the attendant quantifier ambiguity phenomena. The underlying machinery is not of lambda-calculus but of much simpler relational algebra, with the straightforward set-theoretic interpretation.

Slides & Code

Described during the 10-minute short talk: Session types without sophistry

Conor McBride, Bity: Bidirectional Typing (Thursday, March 21, 10:57-:11:52)
At the whiteboard, I presented the basics of a correct-by-construction approach to building type systems in the bidirectional style. In this style, the places in typing judgements each have one of three modes, input, subject, or output. Every input comes with a precondition, namely a judgement for which it is the subject, explaining what must be checked beforehand; every output comes with a postcondition, explaining what is guaranteed by the rules. Below, the subject is given in square brackets: inputs are left of the subject, outputs right. Preconditions and postconditions are in braces.
  • context validity {} [Γ] ⊢ {}
  • type formation {Γ ⊢} Γ ⊢ type [T] {}
  • type checking {Γ ⊢ type T} Γ ⊢ T ∋ [t] {}
  • type synthesis {Γ ⊢} Γ ⊢ [e] ∈ S {Γ ⊢ type S}
  • type equality {Γ ⊢ type S, Γ ⊢ type T} Γ ⊢ S = T [] {}
  • type universe {Γ ⊢ type T} Γ ⊢ univ T [] {}
The structure of the formulae which may appear in typing rules depends on these modes and ensures a proper scoping discipline for schematic variables, which each have one binding site in a pattern, and zero or more use sites. Rule conclusions have patterns for inputs and subjects, but expressions for outputs; rule premises have expressions for inputs, subject pattern variables for subjects, and patterns for outputs. Schematic scope flows clockwise from inputs and subjects of the conlcusion, left-to-right through the premises, then into the outputs of the conclusion. The preconditions tell us what is trusted about pattern variables in conclusion inputs and premise outputs. The pattern variables from conclusion subjects are untrusted and must thus each occur exactly once as a subject premise, in order to establish trust in them and bring them into scope for use in later expressions. This scoping discipline ensures the effectiveness of induction on derivations as a tool for establishing subject reduction, in that premise subjects can compute at most as much as conclusion subjects. Patterns are the fragment of the calculus which is stable with respect to computation: once a term matches a pattern, further computation of that term cannot cause match failure. As a consequence, patterns interrogate only the canonical structure of terms and thus readily admit unification. It is easy to compute the set of possible redexes by unifying the checked type in each introduction rule with the synthesized target type in each elimination rule: separately ensuring that these rule sets are non-overlapping is enough to guarantee that redexes are non-overlapping, giving confluence of reduction by construction.

Meanwhile, the discipline on free variables in the type system under construction is yet more stern: the context is implicitly plumbed through all rules and may only be locally extended in premises; only the variable rule, fixed for all systems, may mention free variables: x ∈ S if x : S is in the context. As substitutions act on free variables, preserving everything else, all expressible type systems are stable under substitution by construction. It is literally impossible to write rules which assert anything falsifiable by the action of a substitution.

The bidirectional approach of checking types for introduction forms and synthesizing them for elimination forms ensures that known types are propagated appropriately into the components of terms, eliminating the need for type annotations in β-normal forms. Type annotations occur only to give the computationally active type in each β-redex. Showing that each β-rule decreases some well founded measure on the computationally active types is sufficient to demonstrate normalisation.

This repository gives the work in progress on the paper and the Agda formalisation.

Photo of Conor, Photo of Whiteboard

Johan Jeuring, Comparing Haskell Programs (Thursday, March 21, 11:54-12:34)

Bernhard Möller, Prim more Primitively? (Thursday, March 21, 14:05-14:53)
We present a new correctness proof for Prim's algorithm. The standard proof establishes the invariant that each iteration constructs a subtree of some minimal spanning tree, and heavily relies on the existence of a spanning tree of the overall graph, as well as an `edge exchange' property, which includes reasoning about graph cycles. We establish a stronger property showing that the algorithm builds a minimal spanning tree in each step, w.r.t. the vertices already covered. As a consequence, the proof does not use the existence of a minimal spanning tree of the entire graph, does not use the classical exchange property.


Shin-Cheng Mu, An Experimental Implementation of Pi-Calculus (Thursday, March 21, 14:54-15:14)
In this short demo by me and Ting-Yan Lai, we would like to show the attendees an implementation of pi-calculus, which is intended to use in the concurrent programming fragments of my undergraduate-level Programming Languages class, such that the students have a tool experiment and play with.


Florian Rabe, Diagram Operators (Thursday, March 21, 15:40-16:12)
Formal libraries, especially large ones, usually employ modularity to build and maintain large theories efficiently.
Although the techniques used to achieve modularity vary between systems, most of them can be understood as
operations in the category of theories and theory morphisms.
This yields a representation of libraries as diagrams in this category, with all theory-forming operations extending
the diagram.

However, as libraries grow even bigger, it is starting to become important to build these diagrams
modularly as well, i.e., we need languages and tools that support computing entire diagrams at once.
A simple example would be to systematically apply the same operation to all theories in a diagram and return both the new diagram and the morphisms that relate the old one to the new one.

In this talk I give an overview of the current state and open problems in defining diagram combinators as an extension to the MMT language and tool.
A first draft paper is available at rabe.pdf

Tarmo Uustalu, Brzozowski and Antimirov for Existentially Regular Trace Languages (Thursday, March 21, 16:16-17:34)

Janis Voigtländer, IO Tasks (Thursday, March 21, 17:43-17:05)

Fritz Henglein, Software Contracts as Contracts (Friday, March 22, 11:40-12:20)

Schedule (subject to change)

Sessions will start at 9:00 on Monday and finish at noon on Friday.

Monday, Tuesday, and Thursday, the schedule is as follows:
  • session – 9:00 to 10:30
  • coffee break – 10:30 to 11:00
  • session – 11:00 to 12:30
  • lunch – 12:30 to 14:00
  • session – 14:00 to 15:30
  • coffee break – 15:30 to 16:00
  • session – 16:00 to 18:00
  • dinner – 18:30 to 19:30
Wednesday and Friday we will have sessions only in the morning:
  • session – 9:00 to 10:30
  • coffee break – 10:30 to 11:00
  • session – 11:00 to 12:30
  • lunch (Wednesday) – 12:30 to 13:30
The Friday-morning session before the 10:30 coffee break is attended by members only.

-- TomSchrijvers - 09 Jul 2018
Topic attachments
I Attachment Action Size Date Who Comment
Dagand.lhslhs Dagand.lhs manage 7 K 19 Mar 2019 - 22:37 TomSchrijvers Pierre-Evariste
HoefnerMoellerSlides.pdfpdf HoefnerMoellerSlides.pdf manage 199 K 21 Mar 2019 - 12:32 BernhardMoeller  
Ko.agdaagda Ko.agda manage 3 K 19 Mar 2019 - 22:38 TomSchrijvers Josh
antoy-long.pdfpdf antoy-long.pdf manage 140 K 19 Mar 2019 - 22:40 TomSchrijvers Sergio
bernhard.pdfpdf bernhard.pdf manage 199 K 21 Mar 2019 - 14:24 TomSchrijvers Bernhard
brent.pdfpdf brent.pdf manage 124 K 22 Mar 2019 - 04:02 TomSchrijvers Brent
brijesh.pdfpdf brijesh.pdf manage 493 K 19 Mar 2019 - 01:20 TomSchrijvers Brijesh
carroll.pdfpdf carroll.pdf manage 875 K 22 Mar 2019 - 04:04 TomSchrijvers Carroll
conor1.jpgjpg conor1.jpg manage 379 K 25 Mar 2019 - 02:39 TomSchrijvers Conor
conor2.jpgjpg conor2.jpg manage 364 K 25 Mar 2019 - 02:39 TomSchrijvers Conor
fritz.pdfpdf fritz.pdf manage 319 K 23 Mar 2019 - 11:15 TomSchrijvers  
janis.pdfpdf janis.pdf manage 164 K 21 Mar 2019 - 14:24 TomSchrijvers janis
johan.pdfpdf johan.pdf manage 815 K 22 Mar 2019 - 04:03 TomSchrijvers Johan
kazutaka.pdfpdf kazutaka.pdf manage 6 MB 19 Mar 2019 - 01:21 TomSchrijvers Kazutaka
marcos.mfmf manage 1 K 21 Mar 2019 - 05:38 TomSchrijvers Marcos
marcos.pdfpdf marcos.pdf manage 116 K 21 Mar 2019 - 05:37 TomSchrijvers Marcos
primes.pdfpdf primes.pdf manage 389 K 22 Mar 2019 - 03:59 JeremyGibbons  
rabe.pdfpdf rabe.pdf manage 316 K 26 Mar 2019 - 15:16 FlorianRabe  
ralf.pdfpdf ralf.pdf manage 94 K 19 Mar 2019 - 22:40 TomSchrijvers Ralf
sam.pdfpdf sam.pdf manage 183 K 22 Mar 2019 - 04:03 TomSchrijvers Sam
shin.pdfpdf shin.pdf manage 32 K 22 Mar 2019 - 04:05 TomSchrijvers Shin
tarmo.pdfpdf tarmo.pdf manage 232 K 22 Mar 2019 - 04:05 TomSchrijvers Tarmo
wg21_mega.pdfpdf wg21_mega.pdf manage 965 K 20 Mar 2019 - 02:22 TomSchrijvers Tom
wg21m78-20190318-edited.pdfpdf wg21m78-20190318-edited.pdf manage 4 MB 19 Mar 2019 - 11:55 JeremyGibbons  
Topic revision: r48 - 05 Apr 2019, ConorMcBride
This site is powered by FoswikiCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding Foswiki? Send feedback