MLscript: Principal Type Inference in a Boolean Algebra of Structural Types
May 16, 2022
What would TypeScript look like if it had been designed with type inference and soundness in mind? We provide one possible answer in MLscript, a programming language with records, generic classes, first-class unions and intersections, instance matching, and ML-style principal type inference. While MLscript is mostly structurally typed, it contains a healthy sprinkle of nominality for classes, which gives it desirable semantics, enabling the expression of extensible variants. Technically, we define the constructs of our language using union, intersection, and complement (or negation) connectives, making sure they form a Boolean algebra, and we show that the addition of a few nonstandard but sound subtyping rules gives us enough structure to derive a sound and complete type inference algorithm. With this work, we aim to disprove a long-held belief that principal type inference is not feasible for programming languages with expressive subtyping systems, and we hope to encourage and help the implementation of better type inference for present and future programming languages.
Speaker: Lionel Parreaux
Implementation of Generational Garbage Collector in and for Stanza Programming Language
April 25, 2022
Stanza in a small functional programming language with extendable syntax, multi-methods, ubiquitous coroutines and automatic memory management. Simple copying collector of the initial Stanza implementation became a performance bottleneck for larger applications. It is replaced by a more sophisticated generational collector. The collector is implemented in low-level subset of Stanza.
Supplementary materials: lbstanza.org
Speaker: Oleg Pliss (JITX, Inc)
How to keep a secret (or forget it) in Agda
April 11, 2022
Static information flow control (IFC) is a program analysis technique used to detect information leaks ("bad flows") in programs. I will give a brief overview of how IFC can be used in typed functional programming languages, such as OCaml or Haskell, and illustrate the connection between static IFC and so-called effect systems, which have traditionally been used to track computational side-effects such exceptions or I/O. To do so, I will show how a simple IFC system can directly be embedded in the purely functional language Agda.
The talk will involve life-coding in Agda, so I assume that the audience has some familiarity with basic functional programming concepts and ideally some experience with one of the aforementioned functional programming languages.
Speaker: Sandro Stucki (Postdoctoral researcher at Chalmers University of Technology)
Bidirectional Type Checking
April 4, 2022
Over last years bidirectional type checking become pretty much default approach. Bidirectional rules are designed in a way that makes type checking syntax-directed, thus providing a straightforward interpretation in a form of an algorithm. We'll take a look at the case of Simply-Typed λ-calculus, contrast traditional presentation with bidirectional one, see an implementation of a corresponding type-checker, discuss possible extensions and criteria for guiding design of bespoke bidirectional systems.
Speaker: Alexander Chichigin (ML engineer @ Calejo)
Rational index of languages with bounded dimension of parse trees
March 28, 2022
We consider two interesting concepts: dimension of a parse tree (Straler number) and the rational index \rho_L of a language L which is defined as an integer function, where \rho_L(n) is the maximum length of the shortest string in the intersection of L and R, over all regular languages R recognized by n-state nondeterministic finite automata (NFA). We investigate the rational index of languages defined by (context-free) grammars with bounded Straler number, and show that it is of polynomial in n.
Speaker: Ekaterina Shemetova (JetBrains Research, SPbAU, SPbSU)
Bottom-Up Synthesis of Recursive Functional Programs
March 21, 2022
We present a novel bottom-up method for the synthesis of functional recursive programs. While bottom-up synthesis techniques can work better than top-down methods in certain settings, there is no prior technique for synthesizing recursive programs from logical specifications in a purely bottom-up fashion. The main challenge is that effective bottom-up methods need to execute sub-expressions of the code being synthesized, but it is impossible to execute a recursive subexpression of a program that has not been fully constructed yet. In this paper, we address this challenge using the concept of angelic semantics. Specifically, our method finds a program that satisfies the specification under angelic semantics (we refer to this as angelic synthesis), analyzes the assumptions made during its angelic execution, uses this analysis to strengthen the specification, and finally reattempts synthesis with the strengthened specification. Our proposed angelic synthesis algorithm is based on version space learning and therefore deals effectively with many incremental synthesis calls made during the overall algorithm. We have implemented this approach in a prototype called Burst and evaluate it on synthesis problems from prior work. Our experiments show that Burst is able to synthesize a solution to 94% of the benchmarks in our benchmark suite, outperforming prior work
Paper: https://www.cs.utexas.edu/~amiltner/burst.pdf
Speaker: Anders Miltner (UT Austin)
Learning Formulas in Finite Variable Logics (POPL'22)
March 7, 2022
We consider grammar-restricted exact learning of formulas and terms in finite variable logics. We propose a novel and versatile automata-theoretic technique for solving such problems. We first show results for learning formulas that classify a set of positively- and negatively-labeled structures. We give algorithms for realizability and synthesis of such formulas along with upper and lower bounds. We also establish positive results using our technique for other logics and variants of the learning problem, including first-order logic with least fixed point definitions, higher-order logics, and synthesis of queries and terms with recursively-defined functions.
Speaker: Paul Krogmeier (PhD student at University of Illinois at Urbana-Champaign, USA)
Paper: https://dl.acm.org/doi/abs/10.1145/3498671
Tagless-Final Style
February 28, 2022
Tagless-final style is a way to implement DSLs embedded into typed programming languages. It is capable to not only express terms of the DSL, but also its type systems, interpreters, compilers, partial evaluators and optimizations. I'll give an introduction to the technique and show some examples.
Additional materials:
Speaker: Ekaterina Verbitskaia
Semantics Modifiers and Reversible Computations: What We Have Been Doing All That Time
February 21, 2022
One of the most spectacular applications of miniKanren, which showcases its potential, is the implementation of relational interpreters. With a relational interpreter for a general-purpose programming language, it becomes possible to evaluate regular programs in this language in relational semantics. A typical example includes a Scheme over miniKanren over Scheme tower of interpreters, and the typical application includes program synthesis (“quines”, “twines”, “trines”, test-based synthesis, etc.) Another use case is turning verifiers into provers using relational conversion —- a direct syntactic transformation of functional programs into corresponding relational ones. In all these cases, the desirable properties of the solutions have to be ad-hoc justified anew. Meantime, at the edge of the century, Robert Glück and Sergey Abramov have developed a general framework of “semantics modifiers” which seems to address all these questions (and some others). In the talk, we give an overview of the semantics modifiers framework, relate it to the problems relevant for the relational programming domain, and discuss how the latter can benefit from the former (and vice versa).
Additional materials:
Speaker: Dmitry Boulytchev
Designing Efficient Systems with Multi-Stage Programming and Other Type-Safe Metaprogramming Techniques
December 20, 2021
In this talk, I will present the results of my PhD at EPFL, Lausanne, which I obtained in 2020.
Software engineering practices have been steadily moving towards higher-level programming languages and away from lower-level ones. High-level languages tend to greatly improve safety, productivity, and code maintainability because they handle various implementation details automatically, allowing programmers to focus on their problem domains.
However, the gains offered by high-level languages are usually made at the cost of reduced performance: higher-level languages usually consume more memory, run more slowly and require expensive garbage-collecting runtime systems. This trend has been worsening with the increasing adoption of the functional programming paradigm by the industry. Modern programmers are thus faced with a dilemma: should they favor productivity and lower maintenance costs at the expense of performance, or should they focus on performance, to the detriments of almost everything else?
The main idea behind my PhD thesis was that we can help solve this dilemma by making advances in type systems, metaprogramming, and compilers technology. In particular, we study how metaprogramming via statically-typed quasiquotation can let programmers define their own domain-specific optimizations in a safe way, while leveraging the latest advances in intermediate program representations.
We will look at the design and implementation of the Squid metaprogramming framework, which extends the Scala programming language with multi-staged programming capabilities and more. We will study a few of Squid's application examples, which include a polymorphic yet efficient library for linear algebra, a stream fusion engine improving on the state of the art, a demonstration of query compilation by rewriting, a staged SQL database system prototype, and a new embedded domain-specific language for expressing queries over collections of data.
Additional materials:
Speaker: Lionel Parreaux
Collaborative Inference of Combined Invariants
December 13, 2021
Program verification techniques can be split into two groups: white-box (like CEGAR, IC3/PDR) and black-box "guess and check" (like ICE, CEGIS, FMF). On the one hand, white-box approaches heavily depend on generalization strategy (e.g., interpolation strength) and the structure of the verified system. On the other hand, black-box learning approaches are tied to the shape of examples from which they learn. In this talk, we will discuss how to obtain a collaborative invariant inference by integrating white-box and black-box approaches. The proposed technique not only combines their pros and mitigates their cons but also allows one to infer rich combined invariants. Their expressiveness is the main reason why the presented technique is also capable of proving the safety of more programs than just an independent run of combined approaches could. We instantiate our technique for one white-box (PDR in SPACER engine in Z3) and one black-box approach (tree automata learning by finite-model finding in RInGen) in the task of proving the safety of programs over algebraic datatypes. Our second instantiation uses the Vampire theorem prover as a black-box invariant "learner" - this shows the flexibility of our technique. Our implementation increased the number of verified programs by Vampire by 30% and by RInGen by 250%.
Speaker: Yurii Kostyukov
Automatic Function Inversion in Haskell
December 6, 2021
We present an approach for automatic function inversion in Haskell. The inverse functions we generate are based on an extension of Haskell’s computational model with non-determinism and free variables. We implement this functional logic extension of Haskell via a monadic lifting of functions and type declarations. Using inverse functions, we additionally show how Haskell’s pattern matching can be augmented with support for functional patterns, which enable arbitrarily deep pattern matching in data structures. Finally, we provide a plugin for the Glasgow Haskell Compiler to seamlessly integrate inverses and functional patterns into the language, covering almost all of the Haskell2010 language standard.
Additional materials:
Speaker: Finn Teegen
Semantics Modifiers and Reversible Computations: What We Have Been Doing All That Time
February 21, 2022
One of the most spectacular applications of miniKanren, which showcases its potential, is the implementation of relational interpreters. With a relational interpreter for a general-purpose programming language, it becomes possible to evaluate regular programs in this language in relational semantics. A typical example includes a Scheme over miniKanren over Scheme tower of interpreters, and the typical application includes program synthesis (“quines”, “twines”, “trines”, test-based synthesis, etc.) Another use case is turning verifiers into provers using relational conversion —- a direct syntactic transformation of functional programs into corresponding relational ones. In all these cases, the desirable properties of the solutions have to be ad-hoc justified anew. Meantime, at the edge of the century, Robert Glück and Sergey Abramov have developed a general framework of “semantics modifiers” which seems to address all these questions (and some others). In the talk, we give an overview of the semantics modifiers framework, relate it to the problems relevant for the relational programming domain, and discuss how the latter can benefit from the former (and vice versa).
Additional materials:
Speaker: Dmitry Boulytchev
Inventing a New One for Teaching and Fun
November 29, 2021
In the talk we share our experience of teaching a compiler construction course using a specifically designed for this purpose programming language. The language plays both roles of instrumental and target one, and we discuss pros and cons of this decision. We describe the language and advertise its features as a "language of choice" for compiler construction. We also present the structure of the course, the structure of the compiler, the implementation techniques we utilized and show how they (should?) work together. Finally, we discuss feedback given by the students, both positive and negative.
Additional materials:
Speaker: Dmitry Boulytchev
An efficient reasoning method on logic programming using partial evaluation in vector spaces
November 22, 2021
In this study, we introduce methods of encoding propositional logic programs in vector spaces. Interpretations are represented by vectors and programs are represented by matrices. The least model of a definite program is computed by multiplying an interpretation vector and a program matrix. To optimize computation in vector spaces, we provide a method of partial evaluation of programs using linear algebra. Partial evaluation is done by unfolding rules in a program, and it is realized in a vector space by multiplying program matrices. We perform experiments using artificial data and real data, and show that partial evaluation has the potential for realizing efficient computation of huge scale of programs in vector spaces.
Speaker: Hien D. Nguyen
Algebraic Path Problems
November 15, 2021
Algebraic path problems can be viewed as a single framework for many problems in computer science. Procedures for solving these problems are built using various algebraic structures (semirings). Among such problems, of course, there are graph analysis problems (the shortest path problem, the problem of finding optimal paths for a given objective function, etc.), as well as, for example, the problem of determining a regular language recognized by a finite automaton. In addition, they include some graph analysis problems whose formulations do not directly involve the concept of a path, such as finding all the bridges and articulation points of a graph. Initially, the procedures for solving these problems were developed independently of each other. When the connection between these methods became clear, various attempts were made to find a common theoretical basis for them. At the seminar, we will discuss what algebraic path problems are, what the theory is behind them, and also consider examples of their application in graph theory, network analysis, and static code analysis.
Additional materials:
* Gunter Rote - Path Problems in Graphs - 1989;
* John S. Baras and George Theodorakopoulos - Path Problems in Networks - 2010
Speaker: Rustam Azimov
The Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory Concurrency
November 8, 2022
Program logics and semantics tell a pleasant story about sequential composition: when executing (S_1; S_2), we first execute S_1 then S_2. To improve performance, however, processors execute instructions out of order, and compilers reorder programs even more dramatically.
In this talk, I will present PwT - a new result to appear at POPL'22. PwT is a compositional model that formalizes the real-world multiple-threaded systems using a logical approach. It enriches the standard event-based approach with preconditions and families of predicate transformers to calculate dependencies between instructions.
First, I will introduce the main challenges of concurrent semantics. Then I will show how concurrent program behaviors are determined by dependencies. Finally, I will demonstrate the basic idea of the logical approach to dependency calculation and support it with several examples.
Speaker: Ilya Kaysin
Universal Quantification and Implication in miniKanren
November 1, 2021
We present constructive universal quantification and implication in miniKanren using the goal constructors (forall (v) domain goal) and (implies goal goal). Our implementation is capable of solving rudimentary logic problems while reasoning about equality, disequality, type constraints, and user-defined relations.
The first ~30-40 minutes of the talk will discuss the key ideas behind these goal constructors. The next ~30-40 minutes will cover some of the implementation challenges and performance challenges. We will run some examples to demonstrate performance characteristics. The final ~10-30 minutes will be informal discussions about future work.
Paper: https://icfp21.sigplan.org/details/minikanren-2021-pa..
Speaker: Lisa Zhang, Ende Jin, Gregory Rosenblatt
Compiling Pattern Matching to In-place Transformation
October 25, 2021
In this talk, I present a joint work with Laure Gonnord and Gabriel Radanne about compiling pattern matching to in-place transformation. We define a bare-bone high level domain specific language to express in-place modifications of data-structures. This language then serves as our basis to analyze how the in-place modifications can be made by computing conflicting memory regions. We can then compute the order in which the memory movements have to be done. Once this order is known we can then proceed to generate code that will perform the transformation. The main goal of this work is to keep the high-level view provided by pattern matching when dealing with data-structure modifications without the need to create a new instance of the data-structure.
Paper: https://hal.archives-ouvertes.fr/hal-03355377
Speaker: Paul Iannetta
Efficient Tree-Traversals : Reconciling Parallelism and Dense Data Representations
October 18, 2022
Recent work showed that compiling functional programs to use dense, serialized memory representations for recursive algebraic datatypes can yield significant constant-factor speedups for sequential programs. But serializing data in a maximally dense format consequently serializes the processing of that data, yielding a tension between density and parallelism. This talk shows that a disciplined, practical compromise is possible. We present Parallel Gibbon, a compiler that obtains the benefits of dense data formats and parallelism. We formalize the semantics of the parallel location calculus underpinning this novel implementation strategy, and show that it is type-safe. Parallel Gibbon exceeds the parallel performance of existing compilers for purely functional programs that use recursive algebraic datatypes, including, notably, abstract-syntax-tree traversals as in compilers.
Paper: https://dl.acm.org/doi/pdf/10.1145/3473596
Speaker: Chaitanya Koparkar
Parsley: A Staged Selective Parser Combinator Library
October 11, 2021
Parsley is a parser combinator that foregoes monadic operations so that it can be processed at compile-time -- with staging (via typed template haskell) -- to produce very fast parsers. Instead it adopts selective operations.
In this talk, I will briefly describe what parser combinators are, describe the high-level design of the library, as well as outlining its current and future capabilities. I will discuss how staging works to optimise the parsers themselves.
Speaker: Jamie Willis
Iris, a Modern Concurrent Separation Logic
September 27, 2021
Этот доклад посвящён фреймворку для доказательства многопоточных программ Iris, связанные с которым работы последние несколько лет регулярно встречаются на ICFP, POPL и PLDI. Мы рассмотрим проблемы, с которыми сталкивается такой фреймворк, и концепцию "коммутативные моноиды как ресурсы, инварианты как глобальное состояние", лежащую в основе Iris; посмотрим на небольшие примеры доказательств. От слушателя ожидается знакомство с тройками Хоара и понятием separation logic.
Tupling via Constructive Algorithmics
September 20, 2021
Tupling is a program transformation technique aimed at eliminating multiple traversals of the same data structures, which is achieved by grouping some recursive function calls into tuples. It was first developed within the fold/unfold framework which introduces a lot of costs and complexities to avoid non-termination and thus is impractical.
In this talk, we are going to consider tupling in the constructive algorithmics framework. By representing recursion explicitly in the form of hylomorphisms and modifying it with a set of calculational rules, it achieves fully automatic, modular, composable program transformations which are cheap to implement.
Semantics of First-order Horn Clause Logic
September 10, 2021
First-order Horn clauses (Horn clause for short) are logic formulae of the shape "A0 <- A1, A2, ..., An" where the A's are atomic formulae of the shape "p(t1, t2, ..., tn)", where the p is a predicate symbol and the t's are first-order terms. A finite set of Horn clauses is called a logic program, which can intuitively encode and solve logic puzzles such as the "N-queens problem". Given a logic program, we are interested in what logical truth can be derived from it, and how to derive the truth; these interests are formally known as (respectively) the "denotational semantics" and "operational semantics" of logic programs. Actually, not all logical deductions terminate (chicken or egg, which comes the first?), and this gives rise to a notion more general than "that which can be derived", viz. "that which cannot be refuted" — we call the two kinds of truth "inductive truth" and "coinductive truth" respectively. A piece of inductive truth is always a piece of coinductive truth, but not vice versa. Correspondingly, the denotational and operational semantics of logic programs can be classified into "inductive" and "coinductive". The denotational semantics enjoy a stronger mathematical flavour, and thanks to that, researchers since as early as 70's are aware of the denotational semantics in both inductive and coinductive senses (as least and greatest fixed points of monotone operators over complete lattices). However, the operational semantics is more algorithm-oriented, and it is only since 2000's that coinductive operational semantics emerge. I shall explain with some more details about these semantics and their interrelationship, and introduce the latest development in coinductive operational semantics, in which I participated.
Speaker: Yue LI
Full reduction at full throttle
April 26, 2021
Внутренняя стратегия вычисления термов в Coq основывается на call-by-value семантике Calculus of Inductive Constructions. Но у этой стратегии есть одна проблема: она не оптимизирована по памяти и времени, поэтому она плохо масштабируется на большие проекты. Поэтому в Coq есть более подходящие для больших проектов стратегии вычисления. Одна из них — native_compute.
В этом докладе мы рассмотрим, как работает эта стратегия вычисления, а именно, посмотрим на то, как эта она переводит термы на языке Gallina в код на OCaml. А в конце посмотрим на то, как работают стратегии вычисления в Coq на различных бенчмарках.
Материалы к докладу:
https://hal.inria.fr/hal-00650940/document
Effective Programming in OCaml
April 12, 2021
Effect handlers have been gathering momentum as a mechanism for modular programming with user-defined effects. Effect handlers allow for non-local control flow mechanisms such as generators, async/await, lightweight threads and coroutines to be composably expressed. The Multicore OCaml project retrofits effect handlers to the OCaml programming language to serve as a modular basis of concurrent programming. In this talk, I will introduce effect handlers in OCaml, walk through several examples that illustrate their utility, describe the retrofitting challenges and how we overcome them without breaking the existing OCaml code. I shall also deep dive into the formal semantics of Multicore OCaml effect handlers in order to illustrate the subtleties in stack management. Our implementation imposes negligible overhead on code that does not use effect handles and is efficient for code that does. Effect handlers are slated to land in OCaml after the addition of parallelism support.
The Fine-Grained and Parallel Complexity of Andersen’s Pointer Analysis
November 15, 2021
Алгоритм Андерсена является распространенным инструментом для анализа указателей. Но теоретическая сложность данного алгоритма является кубической, что потенциально очень печально для практического применения. Однако, если ввести небольшие ограничения, то анализ указателей Андерсена может быть осуществлен менее, чем за кубическое время (время умножения булевых матриц). На семинаре мы разберем данный алгоритм и узнаем при чем здесь язык Дика на одном типе скобок. Помимо этого, используя инструменты fine-grained complexity, мы получим нижние оценки алгоритма Андерсена для общего и частных случаев, а также поговорим о параллельной сложности этого алгоритма.
Материалы к докладу:
Anders Alnor Mathiasen and Andreas Pavlogiannis. 2021. The fine-grained and parallel complexity of andersen's pointer analysis. Proc. ACM Program. Lang. 5, POPL, Article 34 (January 2021), 29 pages. DOI:https://doi.org/10.1145/3434315
Flow2Vec: Value-Flow-Based Precise Code Embedding
March 22, 2021
Flow2Vec — это новый подход в статическом анализе кода, который полагается на методы машинного обучения и запросы с контекстно-свободными (КС) ограничениями на графах. Данный подход позволяет строить embedding кода, который сохраняет ассимитричность графа программы, учитывает информацию о потоках данных и о структуре программы, как о наборе процедур с множеством рекурсивных вызовов функций. Построенный embedding можно использовать в дальнейшем в таких задачах, как обобщение или классификация кода, что значительно повышает точность работы и улучшает основные метрики качества конечных алгоритмов.Мы разберем основные шаги построения подобного embedding'а, применение запросов с КС ограничениями в данном процессе, а также посмотрим на возможные приложения наших новейших результатов для вычисления КС запросов в рассматриваемой области.
Докладчик: Егор Орачев
Материалы к докладу:
1. Yulei Sui, Xiao Cheng, Guanqin Zhang, and Haoyu Wang. 2020. Flow2Vec: value-flow-based precise code embedding. Proc. ACM Program. Lang. 4, OOPSLA, Article 233 (November 2020), 27 pages. DOI:https://doi.org/10.1145/3428301
2. Mingdong Ou, Peng Cui, Jian Pei, Ziwei Zhang, and Wenwu Zhu. 2016. Asymmetric Transitivity Preserving Graph Embedding. In Proceedings of the 22nd ACM SIGKDD International Conference on Knowledge Discovery and Data Mining (KDD '16). Association for Computing Machinery, New York, NY, USA, 1105–1114. DOI:https://doi.org/10.1145/2939672.2939751
3. Arseniy Terekhov, Artyom Khoroshev, Rustam Azimov, and Semyon Grigorev. 2020. Context-Free Path Querying with Single-Path Semantics by Matrix Multiplication. In Proceedings of the 3rd Joint International Workshop on Graph Data Management Experiences & Systems (GRADES) and Network Data Analytics (NDA) (GRADES-NDA'20). Association for Computing Machinery, New York, NY, USA, Article 5, 1–12. DOI:https://doi.org/10.1145/3398682.3399163
4. Egor Orachev, Ilya Epelbaum, Rustam Azimov, Semyon Grigorev. 2020. Context-Free Path Querying by Kronecker Product. https://link.springer.com/chapter/10.1007/978-3-030-5..
Adventures in Property-Based Testing
December 21, 2020
Property-based testing (aka. QuickCheck) is a successful automated testing approach originating in the programming language community (Claessen and Hughes, ICFP'00). It unites the well-known idea of randomized testing with that of ensuring program-specific properties akin to those encountered within verification and theorem proving. Starting as a Haskell library the approach has grown to become language independent with ports to over 30 different programming languages. Over the years property-based testing has been used to pinpoint an impressive amount of software errors in a multitude of settings, initially within academia but more and more so also in the software industry.
In this talk I will first recall the basic concepts of property-based testing and then cover a couple of recent applications, while sharing some of the folklore and community know-how. I will then offer a personal perspective on the approach, both in terms of programming language theory and software engineering.
Speaker: Jan Midtgaard
Event Structures and True Concurrency Semantics for CCS
December 14, 2020
Traditional approach to model concurrency is operational interleaving semantics. In this approach the semantics of parallel processes is defined as an interleaving of their atomic actions. Interleaving semantics present an intuitive and straightforward way to model concurrency. Unfortunately, the reasoning in terms of interleavings is hard for both humans and computers. Besides that, interleaving semantics are not compositional. They cannot be used to define the meaning of the program in terms of its sub-programs.
True concurrency semantics propose an alternative solution. In this framework it is possible to explicitly define the causality relations between atomic actions and avoid the reasoning in terms of all possible interleavings.
In this talk we will consider event structures — one of the classic domains in the theory of true concurrency. We will show how event structures can be used to define denotational (compositional) semantics on the example of Calculus of Communicating Systems (CCS).
Speaker: Evgenii Moiseenko
References:
Winskel G. Event structure semantics for CCS and related languages //International Colloquium on Automata, Languages, and Programming. – Springer, Berlin, Heidelberg, 1982. – С. 561-576.
Winskel G. Event structures //Advanced Course on Petri Nets. – Springer, Berlin, Heidelberg, 1986. – С. 325-392.
Liveness under weak memory
December 7, 2020
Liveness proofs of concurrent programs often rely on thread fairness which is an assumption that every active thread will be eventually scheduled. Yet for execution under weak memory, such requirement turns out to be insufficient; in particular, to prove termination one should also require so-called memory fairness. In this talk, we'll consider how the introduction of such a requirement changes the definitions of common memory models. Also, we will show that for declarative models memory fairness can be defined in a uniform fashion and will use that definition to prove spinlock termination.
Speaker: Egor Namakonov
СFPQ with all-path query semantics
November 30, 2020
At the seminar, we will talk about a matrix algorithm for context-free path querying with all-path semantics, which requires returning all the paths found that match the query. The implementation of this algorithm uses SuiteSparse implementation of the GraphBLAS standard that defines standard building blocks for graph algorithms in the language of linear algebra. We will compare the resulting implementation with the tensor algorithm implementation for all-path semantics.
Speaker: Rustam Azimov
References:
1) Terekhov A. et al. Context-Free Path Querying with Single-Path Semantics by Matrix Multiplication //Proceedings of the 3rd Joint International Workshop on Graph Data Management Experiences & Systems (GRADES) and Network Data Analytics (NDA). – 2020. – С. 1-12.
2) Orachev E. et al. Context-Free Path Querying by Kronecker Product //European Conference on Advances in Databases and Information Systems. – Springer, Cham, 2020. – С. 49-59.
Efficient Fair Conjunction for Structurally-Recursive Relations
November 23, 2020
The relational language miniKanren is designed to be completely declarative, but one of its basic operations --- conjucnction --- has somewhat imperative properties. Both the efficiency and the convergence a conjunction depends on the order of its conjuncts. Therefore, when writing relational program, a user must independently determine the most optimal order in each case.
In the talk we consider a more declarative approach to evaluating relational programs which is insensitive to the order of conjuncts and does not introduce essential performance overhead.
The talk is based on a paper P.Lozov, D.Boulytchev "Efficient Fair Conjunction for Structurally-Recursive Relations", which is accepted for publication to the workshop PEPM 2021.
Speaker: Peter Lozov
References:
P.Lozov, D.Boulytchev "Efficient Fair Conjunction for Structurally-Recursive Relations"
Source-Tracking Unification via Context-Free Path Querying
November 16, 2020
The unification problem is to find a substitution which, being applied to terms, makes them equal. Unification is an integral part of logic programming, type checking and automated theorem provers. Syntactic unification can be expressed as a context-free path querying problem. A path in the graph can serve as a proof that terms can be unified. In the talk we will discuss how to construct a graph for a unification problem, what language can be used as constraints and how to prove that terms can be unified.
Speaker: Ekaterina Verbitskaia
References:
Choppella, Venkatesh, and Christopher T. Haynes. "Source-tracking unification." Information and Computation 201, no. 2 (2005): 121-159.
Relational Synthesis for Pattern Matching
November 9, 2020
In this talk we will give brief overview of modern ways to compile pattern matching. Also, we will present a new approach based on program synthesis.
The talk is based on a paper D.Kosarev, D.Boulytchev "Relational Synthesis for Pattern Matching", which is accepted for publication on the conference APLAS 2020
Definitional Proof-Irrelevance without K
November 9, 2020
It's very well known that formalization of mathematics, logic, programming languages and program verification done within the confines of type theory reveals severe limitations of the hierarchy of equality in it. The minstrels of academia routinely sing us the song of setoid hell and a rare hero fights its consequences with nothing but papers. The more definitionally equal terms we have the easier it gets. Not only we get to write less code, typechecking might even take a little bit less than ages if we use the proof-by-reflection approach. Who cares about proofs? The theory should just decisively squash them together and let us get our subset types without any hassle. But introducing definitionally equal proof terms naïvely is a road to nowhere: we either loose decidability of typechecking or become incompatible with other extensions, especially univalence.
The first act of the talk will introduce and explain the universes of the Coq proof assistant to set the scene for the second act. In the second act we'll get acquainted with a pretty recent experimental addition to the family of Coq's universes, low and behold, our major character -- SProp, a universe of strict propositions. I'll provide a number of examples to illustrate the applicability of SProp, its elimination principles over type, the difference between Sprop and Prop and how all the universes interact.
Speaker: Anton Trunov
References:
1. "Definitional proof-irrelevance without K" - G. Gilbert, J. Cockx, M. Sozeau, N. Tabareau (2019), https://dl.acm.org/doi/10.1145/3290316
2. The Coq Reference Manual: https://coq.github.io/doc/master/refman/addendum/s...