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

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 |

- Membership
- 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.

- M79 (Dec 2019/Jan 2020) Veluwe (NL).
- M80 (Aug 2020) Germany?

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. Slides

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. SlidesKazutaka Matsuda,

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. SlidesJosh Ko,

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. CodePierre-Evariste Dagand,

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. CodeBrent Yorgey,

SlidesSergio Antoy,

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. SlidesSam Lindley,

SlidesMarcos Viera,

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. SlidesRalf Hinze,

SlidesJeremy Gibbons,

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. SlidesTom Schrijvers,

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. SlidesJosé Pedro Magalhães,

SlidesOleg Kiselyov,

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 sophistryConor McBride,

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,Johan Jeuring,input,subject, oroutput. Every input comes with aprecondition, namely a judgement for which it is the subject, explaining what must be checked beforehand; every output comes with apostcondition, 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.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

- context validity {} [Γ] ⊢ {}
- type formation {Γ ⊢} Γ ⊢
type[T] {}- type checking {Γ ⊢
typeT} Γ ⊢ T ∋ [t] {}- type synthesis {Γ ⊢} Γ ⊢ [e] ∈ S {Γ ⊢
typeS}- type equality {Γ ⊢
typeS, Γ ⊢typeT} Γ ⊢ S = T [] {}- type universe {Γ ⊢
typeT} Γ ⊢univT [] {}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 https://github.com/pigworker/TypesWhoSayNi gives the work in progress on the paper and the Agda formalisation. Photo of Conor, Photo of Whiteboard

SlidesBernhard Möller,

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. SlidesShin-Cheng Mu,

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. SlidesFlorian Rabe,

Formal libraries, especially large ones, usually employ modularity to build and maintain large theories efficiently.Tarmo Uustalu,

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

SlidesJanis Voigtländer,

SlidesFritz Henglein,

Slides

- 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

- 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

I | Attachment | Action | Size | Date | Who | Comment |
---|---|---|---|---|---|---|

lhs | Dagand.lhs | manage | 7 K | 19 Mar 2019 - 22:37 | TomSchrijvers | Pierre-Evariste |

HoefnerMoellerSlides.pdf | manage | 199 K | 21 Mar 2019 - 12:32 | BernhardMoeller | ||

agda | Ko.agda | manage | 3 K | 19 Mar 2019 - 22:38 | TomSchrijvers | Josh |

antoy-long.pdf | manage | 140 K | 19 Mar 2019 - 22:40 | TomSchrijvers | Sergio | |

bernhard.pdf | manage | 199 K | 21 Mar 2019 - 14:24 | TomSchrijvers | Bernhard | |

brent.pdf | manage | 124 K | 22 Mar 2019 - 04:02 | TomSchrijvers | Brent | |

brijesh.pdf | manage | 493 K | 19 Mar 2019 - 01:20 | TomSchrijvers | Brijesh | |

carroll.pdf | manage | 875 K | 22 Mar 2019 - 04:04 | TomSchrijvers | Carroll | |

jpg | conor1.jpg | manage | 379 K | 25 Mar 2019 - 02:39 | TomSchrijvers | Conor |

jpg | conor2.jpg | manage | 364 K | 25 Mar 2019 - 02:39 | TomSchrijvers | Conor |

fritz.pdf | manage | 319 K | 23 Mar 2019 - 11:15 | TomSchrijvers | ||

janis.pdf | manage | 164 K | 21 Mar 2019 - 14:24 | TomSchrijvers | janis | |

johan.pdf | manage | 815 K | 22 Mar 2019 - 04:03 | TomSchrijvers | Johan | |

kazutaka.pdf | manage | 6 MB | 19 Mar 2019 - 01:21 | TomSchrijvers | Kazutaka | |

mf | marcos.mf | manage | 1 K | 21 Mar 2019 - 05:38 | TomSchrijvers | Marcos |

marcos.pdf | manage | 116 K | 21 Mar 2019 - 05:37 | TomSchrijvers | Marcos | |

primes.pdf | manage | 389 K | 22 Mar 2019 - 03:59 | JeremyGibbons | ||

rabe.pdf | manage | 316 K | 26 Mar 2019 - 15:16 | FlorianRabe | ||

ralf.pdf | manage | 94 K | 19 Mar 2019 - 22:40 | TomSchrijvers | Ralf | |

sam.pdf | manage | 183 K | 22 Mar 2019 - 04:03 | TomSchrijvers | Sam | |

shin.pdf | manage | 32 K | 22 Mar 2019 - 04:05 | TomSchrijvers | Shin | |

tarmo.pdf | manage | 232 K | 22 Mar 2019 - 04:05 | TomSchrijvers | Tarmo | |

wg21_mega.pdf | manage | 965 K | 20 Mar 2019 - 02:22 | TomSchrijvers | Tom | |

wg21m78-20190318-edited.pdf | manage | 4 MB | 19 Mar 2019 - 11:55 | JeremyGibbons |

Edit | Attach | Print version | History: r48 < r47 < r46 < r45 | Backlinks | View wiki text | Edit wiki text | More topic actions

Topic revision: r48 - 05 Apr 2019, ConorMcBride

Copyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.

Ideas, requests, problems regarding Foswiki? Send feedback

Ideas, requests, problems regarding Foswiki? Send feedback