Bergen Language Design Laboratory (BLDL)
BLDL has an internal meeting series. Some of these have a content which may be of interest to a larger audience. The program of these are announced here.
Contact Magne Haveraaen for more information.
Seminars 2020
- Thursday 2020-09-10 1415-1500,
Zoom
Mikhail Barash (BLDL, University of Bergen)
Specifying Software Languages: Grammars, Projectional Editors, and Unconventional ApproachesI will discuss several approaches for defining software languages, together with Integrated Development Environments for them. Theoretical foundation is grammar-based models: they can be used where proven correctness of specifications is required. From a practical point of view, I'll talk about how language specification can be made more accessible by focusing on language workbenches and projectional editing, and discuss how it can be formalized. I'll also give a brief overview of unconventional ideas to language definition, and outline three open problems connected to the approaches I mention.
- Thursday 2020-10-08 1515-1600,
Zoom
Valery Isaev (JetBrains Research and Saint Petersburg National Research Academic University)
Arend - a Theorem Prover Based on Homotopy Type TheoryI will discuss Arend, a proof assistant developed at JetBrains Research. The aim of Arend is to provide a powerful system for formalization results in homotopy type theory and in ordinary mathematics. To achieve the latter goal, we prove a flexible class system with subtyping, universe polymorphism with a powerful level inference mechanism, quotient sets with convenient pattern matching principles for them. Arend also provides a framework for implementing language extensions, which can be used to implement various problem solvers, tactics and modify the syntax of the language.
Short bio: Valery Isaev is the main designer of the Arend language. He also works on semantics of type theories, higher category theory, and algebraic presentations of type theories.
- Thursday 2020-10-15 1015-1200,
Zoom
Vitaly Bragilevsky (JetBrains and Saint Petersburg State University)
Concurrency in HaskellA guest lecture given at INF214 Concurrent Programming. Recording of the talk is available here.
Short bio: Vitaly Bragilevsky is the author of "Haskell in Depth" (Manning Publications) and a Haskell GHC Steering Committee member.
- Thursday 2020-10-22 1515-1600,
Zoom
Knut Anders Stokke (Department of Informatics, University of Bergen)
Manipulating GUI Structures Declaratively - Thursday 2020-11-05 1515-1600,
Zoom
Mostafa Bakhoday Paskyabi (Department of Geophysics, University of Bergen)
On Simulation Software for Offshore Wind Farms - Thursday 2020-11-26 1515-1600,
Zoom
Håkon Robbestad Gylterud (Informatics, University of Bergen)
Differentiating data structuresIn 2005, Abbot, Altenkirch and Ghani [0] showed how the notion of a container (aka. polynomial functor), allows algebraic reasoning on data structures – such as lists or trees. One such algebraic notion is the differentiation (or hole-punching) operation [1] for containers, which satisfy the familiar laws such as Leibniz rule and the chain rule. Applications of this operation include zippers, which can be used to preserve context when traversing data types in functional programming.
In this talk, I give an informal introduction to differentiation of data structures and how the notion of container (and differentiation) can extended to data structures with symmetries, such as bags, cycles and graph embeddings. The extension to symmetries can be found in my master thesis [2], and is closely related to Joyal's notion of a combinatorial species [3] (in French – an exposition in English was made by Bergeron, Labelle and Leroux [4]).
- Thursday 2020-12-03 1515-1600,
Zoom
Mikhail Barash (BLDL, University of Bergen)
Metaprogramming in C++I will give a summary of Andrew Sutton's proposal P2273R1 (Metaprogramming) for the ISO C++ evolution group (http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2020/p2237r0.pdf, https://github.com/lock3/wg21/tree/main/p2237)