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.

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.

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.

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.

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.

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.

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.

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.

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

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.

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.

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.

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

*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:

- E. W. Dijkstra. Goto statement considered
harmful.
*Commun. of the ACM*, v. 11, n. 3, pp. 147-148, 1968. - R. L. Clarke. A linguistic
contribution to goto-less programming.
*Datamation*, v. 19, n. 12, pp. 62-63, 1973. - P. Abrahamson. Structured programming
considered harmful.
*ACM SIGPLAN Notices*, v. 10, n. 4, pp. 13-24, 1975. - W. Slater, H. Modell.
Structured programming considered harmful.
*ACM SIGPLAN Notices*, v. 13, n. 4, pp. 76-79, 1978. - D. E. Knuth. Structured programming
with goto statements.
*ACM Computing Surveys*, v. 6, n. 4, pp. 261-301, 1974. - F. Rubin. "Goto
considered harmful" considered harmful.
*Commun. of the ACM*, v. 30, n. 3, pp. 195-196, 1987. - D. Moore, C. Musciano, M. J. Liebhaber, S. F. Lott, L. Starr. ""Goto considered
harmful" considered harmful" considered harmful.
*Commun. of the ACM*, v. 30, n. 5, pp. 351-355, 1987. - R. Hindle. Goto and comefrom for Python. 1 April 2004.
- F. X. Reid. On the formal
semantics of the comefrom statement.
*FACS FACTS*, n. 2006-1, pp. 18-21, 2006. See also: V. Zemantics. Obituary: F. X. Reid.*FACS FACTS*, n. 2006-1, pp. 12-14, 2006.

Aivar Annamaa

Tarmo Uustalu

Varmo Vene

Viimane uuendus 8.02.2010