Bei Fragen: MIT MAUSZEIGER LESBAR MACHEN! lennart
. beringer { Klammeraffe } ifi PUNKT lmu PUNKT de
Hier können Sie die Oberseminar-Ankündigungen per E-mail bestellen.
17.10. Igor Razgon: Fixed-Parameter Tractability of 2-CNF Deletion problem
24.10. NN
31.10. Kein Vortrag (Abschiedskolloquium Prof. Hegering)
05.11. Extra-Vortrag: Mathijs de Weerdt
07.11. Kein Vortrag (Medizininformatik-Workshop)
12.11. Extra-Vortrag: Colin Riba
14.11. Kein Vortrag (PUMA-Workshop)
19.11. Extra-Vortrag: Davide Grossi: Correspondences in the Theory of Aggregation
21.11. Ulrich Schöpp: A Formalised Lower Bound on Undirected Graph Reachability
28.11. Philip Wassenberg (DA):
Implementation and Evaluation of Cryptographic Auction Protocols,
Sarah Bluhme (FoPra):
Implementierung von Algorithmen zur Berechnung von Turnierl&oml;sungen mit Benutzeroberfläche
05.12. Dulma Rodriguez: Verification of an algorithm for computing greatest fixpoints in Coq
12.12. NN
19.12. Andreas Abel: Normalization by Evaluation for System F
09.01. Jan Hoffmann: Automatic Amortized Analysis for Polynomially Bounded Resources
16.01. Paul Harrenstein
23.01. Martin Hofmann
30.01. Robert Grabowski
06.02. Roland Axelsson
Es spricht: Jan Hoffmann
LFE Theoretische Informatik, LMU
über: Automatic Amortized Analysis for Polynomially Bounded Resources
==============================================================
Inhalt: In 2003 Hofmann and Jost introduced an automatic amortized
analysis to obtain bounds on the resource consumption of functional
programs. They have shown that type systems and linear programming
can be used to compute these bounds fully automatic without requiring
any annotations in the program.
Such a static automatic amortized analysis can been applied to many
standard algorithms such as quicksort and is able to obtain bounds on
the run time, the heap space and the stack space needed by the
algorithm. It is efficiently computable and does not affect the run
time behavior of the program. As yet, the drawback of this method was
its limitation to resource bounds that are linear in the input.
We show how to overcome this drawback by presenting an extension to
the previous systems that is able to compute resource bounds on
functional programs whose resource consumption is polynomial in the
input.
Es spricht: Andreas Abel
LFE Theoretische Informatik, LMU
über: Normalization by Evaluation for System F
========================================
Inhalt: Normalization by evaluation is a technique to compute the full
beta-normal form of lambda-terms. In the first step, terms are
interpreted in some value domain, which corresponds to computing a
semantic weak head normal form. In the second step, values are
reified, i.e., converted back to terms which are actually normal forms.
During reification, evaluation under binders takes place.
In this talk, I will first give a tutorial on normalization by
evaluation for the simply-typed lambda-calculus. I review
interpretation of lambda-terms into an applicative structure and then
define a simple type-directed reification which returns eta-long
beta-normal forms. I sketch the proof of soundness and completeness
which involves constructions of Kripke logical relations. The proof
is generic enough to account for related results, like weak
beta-(eta-)normalization.
In the last part of my talk, I outline how to extend normalization by
evaluation to System F, the polymorphic lambda-calculus, using
Girard's idea.
Es spricht: Dulma Rodriguez
LFE Theoretische Informatik, LMU
über: Verification of an algorithm for computing greatest fixpoints in Coq
========================================
Inhalt:
We present an algorithm for computing membership in the greatest fixpoint of
a monotone operator on the powerset of some given set. Rather than
computing the entire fixpoint by Knaster-Tarksi iteration we
depart from a given goal. This is maybe advantageous if the size of the
underlying set or of the greatest fixpoint is large compared to the
portion that is relevant for determining membership of a particular
element. We prove this algorithm sound and complete and present a
verification of the proof in the theorem prover Coq.
Es sprechen Philip Wassenberg
LFE Theoretische Informatik, LMU
über: Implementation and Evaluation of Cryptographic Auction Protocols (Diplomarbeit)
und Sarah Bluhme
LFE Theoretische Informatik, LMU
über: Implementierung von Algorithmen zur Berechnung von Turnierl\ouml;sungen mit Benutzeroberfläche (FoPra)
Es spricht: Ulrich Schöpp
LFE Theoretische Informatik, LMU
über: A Formalised Lower Bound on Undirected Graph Reachability
========================================
Inhalt: We consider the expressivity of Jumping Automata on Graphs (JAGs), an
idealised model of computation with logarithmic space. JAGs operate on
graphs by using finite control and a constant number of pebbles. In this
talk we revisit the proof of Cook & Rackoff that JAGs cannot decide
s-t-reachability in undirected graphs. Cook & Rackoff prove this result
by constructing, for any given JAG, a finite graph that cannot be
traversed exhaustively by the JAG. We generalise this result from the
graphs constructed by Cook & Rackoff to a general class of group action
graphs. We establish a bound on the number of nodes that a JAG can visit
on such action graphs. This generalisation allows us to strengthen the
result of Cook & Rackoff to the existence of a graph of small degree
whose diameter (rather than its number of nodes) is larger than the
number of nodes the JAG can visit. In this talk I will report about a
formalisation of the main result in the theorem prover Coq, using
Gonthier's tactic language SSReflect.
Es spricht: Davide Grossi
Individual and Collective Reasoning Group,
Computer Science and Communications,
University of Luxembourg
über: Correspondences in the Theory of Aggregation
=========================================
Inhalt: In this talk I will investigate some interrelationships between the
social-theoretic problems of preference and judgment aggregation from
the perspective of formal logic. On the one hand, preference
aggregation will be shown to be equivalent to the aggregation of some
special types of judgments (logical formulae). On the other hand, the
judgment aggregation problem will be proven equivalent to the
aggregation problem of specific types of preferences. As a result, a
detailed map of aggregation problems is obtained which better
highlights differences and similarities between the two research
fields of preference and judgment aggregation, and which makes a
unified systematization of the two fields possible.
Es spricht: Colin Riba, INRIA Sophia Antipolis
über: Type-based termination with sized products
========================================
Inhalt: Type-based termination is a semantically intuitive method
that ensures termination of recursive definitions by tracking the size
of datatype elements, and by checking that recursive calls operate on
smaller arguments. However, many systems using type-based termination
rely on a semantical anomaly to guarantee strong normalization;
namely, they impose that non-recursive elements of a datatype, e.g. the
empty list, have size 1 instead of 0. This semantical anomaly also
prevents functions such as quicksort to be given a precise typing.
The main contribution of this paper is a type system that remedies this
anomaly, and still ensures termination. In addition, our type system
features prenex stage polymorphism, a weakening of existential
quantification over stages, and is precise enough to type quicksort as a
non-size increasing function. Moreover, our system accommodate stage
addition with all positive inductive types.
Es spricht: Mathijs de Weerdt
über: A strategy-proof auction mechanism without money
========================================
Inhalt: I'll start this talk by briefly discussing Vickrey's
well-known sealed- bid second-price auction, and illustrate this type
of auction by noting the similarity to eBay's bidding proxy. I'll show
that (under ideal circumstances) bidding your private value is a
dominant strategy in this auction.
After this introduction I'll propose a new similar mechanism but
without money. In this mechanism a bid can be any alternative, rather
than just a monetary offer. Such an auction is applicable to
situations where no numeraire is available, when there is a fixed
budget, or when money is no issue. Finally I'll discuss some of the
properties and variants of this mechanism.
Es spricht: Igor Razgon
über: Fixed-Parameter Tractability of 2-CNF Deletion problem
========================================
Inhalt: Fixed-parameter algorithms provide an alternative methodology
of coping with NP-hardness that allows to solve hard optimization
problems exactly and in a low-polynomial time. The necessary
condition for design a fixed-parameter algorithm is the presence of a
parameter associated with the given problem. The time complexity of a
fixed-parameter algorithm can be represented in a form $O(f(k)*n^c)$,
where $k$ is the parameter, $f(k)$ is an exponential function on the
parameter, $c$ is a constant usually not greater than 3. Thus a
fixed-parameter algorithm is exponential in the parameter but
polynomial in the input size. The low-polynomial time is achieved for
small values of $k$.
The design of fixed-parameter algorithms was inspired by observation
that in areas like bioinformatics and network design many hard
problems are associated with natural parameters that in practice are
very small.
Problems that admit fixed-parameter algorithms are called
fixed-parameter tractable (FPT) and the area of Theoretical Computer
Science studying various aspects of fixed-parameter tractability and
intractability is called Parameterized Complexity. One of the key
question investigated in the area is classification of problems
i.e. telling whether a particular problem is FPT. The community
identified a number of most challenging open question related to
classification of problems. One of such question is understanding
whether the following problem is FPT: given a 2-CNF formula, is it
possible to remove at most $k$ clauses so that the resulting formula
becomes satisfiable? This problem is called 2-CNF deletion. It
attracted attention of researchers due to a large number of potential
applications of this problem. Despite a number of attempts to solve
the problem, the status of fixed-parameter tractability of the problem
remained unresolved for more than 10 years. The fixed-parameter
tractability of the problem has been confirmed in Razgon, O'Sullivan
"Almost 2-SAT is fixed-parameter tractable", ICALP 2008.
In this talk I will briefly introduce the are of parameterized
complexity and overview main ideas of the fixed-parameter algorithm
for the 2-CNF deletion problem. The talk is designed for the audience
completely unfamiliar with the area of Parameterized Complexity.
Vorträge
in früheren Semestern
Neben dem Oberseminar fand in früheren Semestern
auch noch der Lambda-Kalkül-und-Typen-Club statt,
der jetzt in dieses integriert wurde.