Ettekanded / Talks

Aivar Annamaa: Modular static analysis for object-oriented programs

Ettekande kiled. [pdf]

Abstract: Among the most popular features of modern IDE-s are different kinds of "live" program analysis, running continuously in the background while programmer is editing the code, giving fast feedback about possible errors. In such situation, the performance requirements for analysis procedure are much higher than in traditional "batch mode" setup. Live analysis could be faster, if it were modular -- ie. if after each code modification, only respective part of the program (eg. method or module) needed re-analyzing. This talk describes some common problems in modular static analysis for object-oriented programs and reviews some solutions proposed in recent literature.

Oleg Batrašev: Semi-automatic parallelization of iterative solvers

Ettekande kiled. [pdf]

Abstract: Scientific computing has a set of iterative algorithms for solving large sparse systems of linear equations - iterative solvers. These algorithms are equiped with preconditioners - set of initial matrix transformation techniques to make solvers faster. Parallelization of the preconditioners for multiple processors blows up the code size and messes up the initial algorithm. The parallelization is not trivial, because it contains indirect array accesses through index arrays, that are known only at run time. In this talk, I present some ideas on automatic parallelization of this type of algorithms using static code analysis.

Andrey Breslav: Automatically introducing templates in Domain-Specific Languages

Ettekande kiled. [pdf]

Abstract: Most languages provide some means for reuse. Besides abstraction designed for this purpose, such as functions or classes, some more generic means are used. The characteristic feature of such mechanisms is that they do not affect execution, working merely inside the compiler front-end. The most well-known example will be the cpp preprocessor delivering macros to C. Hygienic macros of LISP and its successors are also relevant here. In fact, even C++ templates are mostly of the same kind, and we refer to the whole class of such mechanisms as "templates".

In this talk I will present a technique for automatically augmenting domain-specific languages with templates which guarantee some amount of structural correctness upon instantiation. We will also discuss some more advanced constraints, such as treating names hygienically.

James Chapman: A biased history of equality in type theory

Ettekande kiled. [pdf]

Abstract: In this talk I will attempt to review the thorny and unfinished issue of equality in Martin-Löf's theory of types. I will explain definitional and propositional equality, intentional and extensional equality, proof irrelevance, homogeneous and heterogenous equality, roll-your-own and built-in equality, setoids, and observational equality.

Grigory Fedyukovich: A Coq formalization of an analysis and optimization of While

Ettekande kiled. [pdf]

Abstract: I present ongoing work with Keiko Nakata and Tarmo Uustalu to formalize analyses and optimizations for the While language with the Coq proof assistant. I use Coq's feature of inductive definitions to formalize the syntax, semantics and Hoare logic of While. I then develop type systems for live variables analysis and dead code elimination and soundness proofs of these type systems against a relational interpretation of types, following the exposition of Tarmo Uustalu and Ando Saabas.

Davide Grohmann: Multi-structure frameworks as adhesive fibrations

Ettekande kiled. [pdf]

Abstract: We present a general setting where adhesive categories can be composed by means of suitable operations; this allows to build more complex, multi-graphical structures starting from simpler ones. We show that, under suitable conditions, the construction of relative pushouts in the composed categories can be obtained from the RPO constructions in the respective components. Previous bi-graphical structures, such as pure and directed bigraphs, can be recovered in this way, but also new and more general structures (e.g., "tri-graphs") can be obtained. Therefore, using these constructions we can build new frameworks where, similarly to bigraphs, computational models can be represented and for which we can derive the IPO labelled transition systems.

Jevgeni Kabanov: Retroactive API Extensions Using Bytecode Weaving

Ettekande kiled. [pptx]

Abstract: One of the uses of Bytecode instrumentation is integration with various systems, for which the source code is either not available or cannot be changed. In this paper we examine how bytecode weaving can be used to retroactively create a unified API that other systems can use for integration purposes without any knowledge of the underlying implementation. We draw on the experience gathered while designing and developing the JRebel product and integrating it with a multitude of different systems. We review two case studies: the extensions to ClassLoader API and Java EE API. These extension are also available as Open Source projects as part of the JRebel product.

Marino Miculan: A bigraphical framework for protein and membrane interactions

Ettekande kiled. [pdf]

Abstract: We introduce the Bioß Framework, a meta-model for both protein-level and membrane-level interactions of living cells. This formalism aims to provide a formal setting where to encode, compare and merge models at different abstraction levels; in particular, higher-level (e.g. membrane) activities can be given a formal biological justification in terms of low-level (i.e., protein) interactions. A Bioß specification provides a protein signature together a set of protein reactions, in the spirit of the κ-calculus. Moreover, the specification describes when a protein configuration triggers one of the only two membrane interaction allowed, that is "pinch" and "fuse". In this paper we define the syntax and semantics of Bioß, analyse its properties, give it an interpretation as biobigraphical reactive systems, and discuss its expressivity by comparing with κ-calculus and modelling significant examples. Notably, Bioß has been designed after a bigraphical metamodel for the same purposes. Hence, each instance of the calculus corresponds to a bigraphical reactive system, and vice versa (almost). Therefore, we can inherith the rich theory of bigraphs, such as the automatic construction of labelled transition systems and behavioural congruences.

Keiko Nakata: Securing class initialization

Ettekande kiled. [pdf]

Abstract: Language-based information-flow security is concerned with specifying and enforcing security policies for information flow via language constructs. Although much progress has been made on understanding information flow in object-oriented programs, the impact of class initialization on information flow has been so far largely unexplored. In this talk I turn the spotlight on security implications of class initialization. We discuss the subtleties of information propagation when classes are initialized and propose a formalization that illustrates how to track information flow in presence of class initialization by a type-and-effect system for a simple language. I show how to extend the formalization to a language with exception handling. (Joint work with Andrei Sabelfeld.)

Härmel Nestra: Implementing Global Variables in Functional Programming

Ettekande kiled. [pdf]; kood [zip]

Abstract: This talk explains the problem of implementing global variables within the functional programming paradigm. The idea of global variable state that looks trivial within imperative programming paradigm turns out to be surprisingly hard to solve within functional programming. Simply using IO monad is not satisfying. We look through 5 different approaches to address the problem.

Martin Pettai: Untyped general polymorphic functions

Ettekande kiled. [pdf]

Abstract: In statically typed functional languages, functions are required to have a type. This also applies to polymorphic functions. If we allow not only parametric polymorphism but also ad-hoc polymorphism with type-level recursion then the types of polymorphic functions will be recursive and very complicated. Thus the type system and type inference algorithm will be very complicated and difficult to implement.

We propose a solution to this by allowing untyped functions that can only branch and recurse on static (type-level) information. This is enough to define very general polymorphic functions, including higher-order polymorphic functions, but it allows all applications of untyped functions to be reduced during the compile time. Thus all types can still be checked during the compile time and no run-time type errors can occur. We have not (yet) been able to prove the decidability of type checking (but if the type checking terminates then the program is type-correct). Maybe it is necessary to add some more restrictions to make type checking decidable.

Sander Sõnajalg: Validating Javascript from Realworld Websites in a Browser-like Environment

Ettekande kiled. [pdf]

Abstract: Javascript is an essential part of today's web applications, Javascript makes possible rich internet applications (RIAs) that run straight in the browser, not in some proprietary closed-source semi-standard plugin or addon. As of today Javascript is an essential part of any web information system project, and that kind of projects usually exercise complicated project automation and quality assurance techniques (like nightly builds with compile-time checks and automated tests) to ensure high quality, fast feedback for errors and lessen the manual testing need. That raises a strong need to create some automated validity checks also for the Javascript part of the application.

Being one of the most dynamic programming languages, it also poses one of the toughest challenges for applying any static analyses to it. The approach taken is to use a Javascript engine (Rhino) to first parse and analyze the scripts and apply some trivial static analyses to it. In the second phase, the execution in the real browser is simulated in a browser-like environment to perform additional analyses that would have been very hard to do statically, and extra information is captured to give a more sophisticated estimation on the correctness of the scripts in different browsers. In particular, the execution simulation can help to estimate the exact types of variables in the code, which is rather hard to do statically.

Ilja Tšahhirov: Proving the Correctness of Dependency Graph Transformation

Ettekande kiled. [ppt]

Abstract: Dependency graphs can be used for reasoning about the properties of a security protocol. The analysis starts with representing the protocol as a dependency graph and goes on with transforming it until its transformed version can be shown to be secure. A single transformation in the transformation sequence corresponds to the replacement of a local fragment in the current graph. The validity of the transformation is based on the assumption that the two local fragments have equivalent semantics. In this talk, I will give an overview of the steps that were taken towards producing the machine-checkable proofs that two graph fragments have equivalent semantics. I will introduce a formal definition of the graph semantics, and will present the currently achieved results. I will conclude my talk with the overview of the next steps that should be taken for verifying the whole analysis technique formally. (Joint work with Peeter Laud and Keiko Nakata).

Tarmo Uustalu: Comefrom considered instructive (Interactive Seminar)

Abstract: We will wrap our minds around the semantics and logic of control flow. In particular, we will try to make sense out of the comefrom construct of R. L. Clark (1973), with variations. We may even ask whether comefrom has or hasn't anything to do with aspect-orientation.

Background reading:

Aivar Annamaa
Tarmo Uustalu
Varmo Vene
Viimane uuendus 8.02.2010