2006
Henk Barendregt - Topics in Typed Lambda
Calculus - 14 March 2006
2005
Tonny Hurkens - Phinary Numbers -
6 December 2005
Iris Loeb and Herman Geuvers
(Radboud Universiteit Nijmegen) - Natural deduction via
graphs - 15 November 2005
Smile Markovski (Ss. Cyril and
Methodius University, Skopje, Macedonia) - Applications of
Quasigroup String Transformations in Cryptography and Coding Theory - 1
November 2005
Ronald Middelkoop - Cooperation-Based
Invariants for OO Languages - 18 October 2005
Lionel Mamane - Surreal Numbers in Coq
and Type Theory - 7 June 2005
Peter van Rossum - MathSAT - combining
Boolean satisfiability solving and mathematical reasoning - 24 May 2005
J-J.Ch. Meyer - On the Semantics of
(Multi) Agent Programming - 26 April 2005
Jan van Eijck - Logics for Epistemic
Updating - 8 March 2005
Russell O'Connor - Incompleteness Proof in
Coq - 8 February 2005
Erik Poll - The type system of
Axiom - 11 January 2005
2004
Francien
Dechesne - IF-logic
from a game-theoretical perspective - 14 December 2004
Ana Sokolova - Weak bisimulation for
action-type coalgebras - 30 November 2004
Georgi Jojgov - A stepwise approach to
formalizing mathematics - 9 November 2004
Jan Hidders - Deciding static
properties of XPath expressions - 5 October 2004
Suzana Andova - Equivalences for silent
transitions in Probabilistic Systems - 29 June 2004
Clemens Grabmayer - Derivability and
admissibility of inference rules in abstract Hilbert systems - 22 June
2004
Martijn Oostdijk - Tool support for
developing JML specs - 8 June 2004
- Automath Symposium
- 26 May 2004
Jesper Carlström (Stockholm,
Nijmegen) - Interpreting
descriptions in intensional type theory - 20 April 2004
Gilles Dowek (France) - Cut elimination for
axiomatic theories - 6 April 2004
Luís Cruz-Filipe - Formalizing
Constructive Mathematics in Type Theory - 16 March 2004
Jos Baeten - A Brief History of
Process Algebra - 2 March 2004
Georgi Jojgov - A Calculus of Tactics
and Its Operational Semantics - 3 February 2004
Peter Grünwald - Shannon information and
Kolmogorov Complexity - 20 January 2004
2003
Patrik Eklund (Finland) - Partial orders make
monads even more useful - 2 December 2003
Paul Harrenstein - Logic in equilibrium
and equilibrium in logic - 25 November 2003
Suzana Andova - Discrete-time rewards
model-checked - 4 November 2003
Bas Luttik - Unique Decomposition -
21 October 2003
Joop Niekus (UvA) - Individual Choice Sequences
in the work of Brouwer - 17 June 2003
Ling Cheung (KUN) - Concise Graphs and
Functional Bisimulations - 3 June 2003
Ana Sokolova (TU/e) and Falk
Bartels (CWI) - A hierarchy of
probabilistic system types - 20 May 2003
Bas Spitters (KUN) - Constructive and
Computer mathematics - 6 May 2003
Maarten Marx (UvA) - Tableaux for Quantified
Hybrid Logic - 8 April 2003
Barteld Kooi (RUG) - Probabilistic Dynamic
Epistemic Logic - 11 March 2003
Mirna Bognar (Deloitte &
Touche, previous affiliation: VU) - The context cube: the
lambda cube with contexts - 25 February 2003
Vincent van Oostrom and Dimitri
Hendriks (UU) - "adbmaL" -
11 February 2003
Pedro d'Argenio (Universidad
Nacional de Cordoba, Argentina) - Reachability Analysis
of Probabilistic Systems by Successive Refinements - 28 January 2003
2002
Sandro Etalle (Twente
University) - A
constraint based system for the verification of security protocols - 10
december 2002
Marc Pauly (University of
Liverpool) - Towards
the Formal Verification of Social Mechanisms - 26 November 2002
Jesse Hughes (KUN) - The Coinductive
Approach to Verifying Cryptographic Protocols - 12 November 2002
Jerry den Hartog - Smartcard security:
Attacking the implementation. - 16 July 2002
Martijn Oostdijk (KUN) - Formal Verification of
a Simple Java Card Payment Applet - 2 July 2002
Francien Dechesne - Logic and game theory:
Hintikka's Independence Friendly Logic - 18 June 2002
|
Date: |
|
|
Title: |
Topics in Typed Lambda Calculus |
|
Speaker(s): |
Henk Barendregt |
Note: The ZIC
colloquium started in september 1986, and this will be the 250th talk in this
series! In the light of several developments, and because it is always good to
end on a high note, we have decided to let this 250th talk be the final one. To
say goodbye to the ZIC and to celebrate its succesful history, this last talk
will be a special event.
|
Abstract: After the untyped lambda
calculus, the typed one seems to be quite restricted. This is not so. Having
dependent types one can formalize mathematics, whereby statements become
types and proofs terms. But already the much more modest type systems of
simple, recursive and intersection types, the topics of a forthcoming book,
provide interesting results. The talk will give examples of these. The simple types are freely
generated from atomic types by the operator -> for function space types.
Many open problems have been settled except the one whether general pattern
matching, $\exists X.FX=G$, is decidable. In the recursive types one
imposes (in)equalities between the freely generated ones. Non-decidable
properties of terms like being strongly normalizable become characterizable
by these types. When intersections of two
types are required to exist, then one can give type theoretic descriptions of
well-known models of untyped lambda calculus. This happens via a general
duality result between (finitary) meet semi-lattices and the much richer
algebraic lattices. |
|
Date: |
|
|
Title: |
Phinary Numbers |
|
Speaker(s): |
Tonny Hurkens |
|
Abstract: The binary number system is
based on the classical fact that e.g. the interval [0, 1] is the union of two
intervals of size 1/2. Constructively this is not valid, but overlapping
subintervals will do. If one takes as size the golden ration phi (given by
phi + phi*phi = 1), then the size of the overlap is phi*phi*phi. This leads
to the phi(nary) number system, see www.mcs.surrey.ac.uk/Personal/R.Knott/Fibonacci.
We also consider a variant with three subintervals of size phi*phi, which
leads to a symmetric representation of integers. |
|
Date: |
|
|
Title: |
Natural deduction via graphs |
|
Speaker(s): |
Iris Loeb and Herman Geuvers (Radboud Universiteit
Nijmegen) |
|
Abstract: We introduce the formalism
of "deduction graphs" as a generalisation of both Gentzen-Prawitz
style natural deduction and Fitch style flag deduction. The advantage of this
formalism is that subproofs can be shared, like in flag deductions (and
unlike natural deduction), but also that the linearisation used in flag
deductions is avoided. Our deduction graphs have both "nodes" and
"boxes", which are collections of nodes that also form a node
themselves. In the first hour we give a
precise definition of deduction graphs and we give examples to illustrate
them. We also show the connections with other natural deduction formalisms.
Gentzen-Prawitz style natural deductions and Fitch style flag deductions can
easily be embedded into the deduction graph formalism. A more interesting
formalism is "proof nets" (the `natural deduction variant' of
linear logic), which also has the notion of "box": we indicate how
to translate deduction graphs to proof nets. In the second hour we study
the computational behaviour of deduction graphs by analysing the process of
cut-elimination and by defining translations from deduction graphs to simply
typed lambda terms. From a slight variation of this translation we conclude
that the process of cut-elimination is strongly normalising. The translation
to simple type theory removes quite a lot of structure and we therefore also
propose a translation to a context calculus with lets, that faithfully
captures the structure of deduction graphs. Finally, we look again into the
translation to proof nets and we connect the process of cut-elimination on a
deduction graph to cut-elimination on its translation. |
|
Date: |
|
|
Title: |
Applications of Quasigroup String Transformations in
Cryptography and Coding Theory |
|
Speaker(s): |
Smile Markovski (Ss. Cyril and Methodius University,
Skopje, Macedonia) |
Note: Prof. Markovski will be our guest on the
occasion of Ana Sokolova's PhD-defense on Thursday November 3.
|
Abstract: Quasigroups are simple
algebraic structures consisting of a set, Q, and a binary operation, *: Q2
Q. The pair (Q,*) is said to be a quasigroup if the equations a * x = b and y * a = b have unique solutions x and
y for each a, b in Q. They are generalization of the groups as algebraic
structures, and of the Latin squares as combinatorial structures, since the
main body of the multiplication table of a finite quasigroup is a Latin
square (every row and column contain different elements). These facts play an
important role in the application of quasigroups. Given a finite quasigroup
(Q, *), |Q| < ∞, several permutations Qn Æ Qn
can be defined, where n is a positive integer. The elements of Qn
can be considered as words (messages) of length n in the alphabet Q. We use
them for suitable definitions of encryption/decryption functions, one way
functions, hash functions, stream ciphers, almost random codes, PRNG, for
repairing of MD4, MD5, SHA, ¿ Several products are designed that way and some
of them are used in industry or are under patent. Keywords: quasigroup,
cryptography, stream cipher, hash function, PRNG, random code |
|
Date: |
|
|
Title: |
Cooperation-Based Invariants for OO Languages |
|
Speaker(s): |
Ronald
Middelkoop |
|
Abstract: A class invariant describes
the consistent states of objects instantiated from that class. In general,
such an invariant can relate the state of several objects. We introduce an
approach that allows this for objects of mutually visible classes, in a way
that supports modular verification. In particular, invariants expressing non-hierarchical
object relations are supported. To this end, dependencies
are made explicit by cooperation. Furthermore, a method can specify
explicitly that it does not depend on the validity of a certain invariant.
Such a method can be called even when that invariant is violated. This allows
a novel, flexible semantics of invariants that still captures their intuitive
meaning. |
|
Date: |
|
|
Title: |
Surreal Numbers in Coq and Type Theory |
|
Speaker(s): |
|
Abstract: Surreal Numbers form a
totally ordered (commutative) Field, containing copies of the reals and (all)
the ordinals. The natural presentation of surreal numbers uses an
induction-recursion scheme, which is not available in Coq. However, the
original presentation by Conway explicitly works around needing
induction-recursion, too. I have encoded most of the Ring structure of
surreal numbers in Coq. This encoding relies on Aczel's encoding of set
theory in type theory. The definition of the order, a direct inductive
definition in Conway's presentation, needed to be separated into a mutually
inductive definition of "at most" and "not at least" to satisfy
Coq's positivity criterion. The recursion and induction schemes used in
definitions and proofs turned out to be too subtle for Coq to accept straight
away. In this talk, I'll present
surreal numbers and the encoding in Coq thereof I made during my Master's at
the TU/e and refined during my PhD at the Radboud Universiteit Nijmegen. I'll
also say a few words about the situation with other theorem provers, mostly
Agda. |
|
Date: |
|
|
Title: |
MathSAT - combining Boolean satisfiability solving and
mathematical reasoning |
|
Speaker(s): |
|
Abstract: Recent improvements in
propositional satisfiability techniques have made it possible to tackle some
hard real-world problems (e.g., model checking of circuit designs,
propositional planning) by encoding them into SAT. However, a purely Boolean
representation is not expressive enough for certain real-world problems
(e.g., verification of timed and hybrid systems) and for other problems
translating into a purely Boolean formula is very inefficient (e.g., circuit
designs that involve arithmetic). At ITC-Irst in Trento, we
developed MathSAT, a satisfiability checker that combines propositional
satisfiability with real and integer arithmetic, allowing for a natural
modelling of the above-mentionned problems. I will discuss the basic
techniques for combining propositional and mathematical reasoning used in
MathSAT. |
|
Date: |
|
|
Title: |
On the Semantics of (Multi) Agent Programming |
|
Speaker(s): |
|
Abstract: Agent(-oriented) Programming is a
programming paradigm in which one tries to realise intelligent systems using
cognitive notions such as beliefs, goals, plans,... Agent-oriented
programming languages have been devised to enable programming directly in
terms of these cognitive notions. Furthermore, to program multi-agent systems
concepts and techniques from concurrent and distributed programming are
added, such as parallel execution, communication, coordination, ... In this
talk I'll briefly discuss the ideas behind agents and agent programming more
in general, after which I'll turn to some more detailed issues, and
semantical ones in particular, centered around the language 3APL developed in
Utrecht. |
|
Date: |
|
|
Title: |
Logics for Epistemic Updating |
|
Speaker(s): |
Jan van
Eijck |
|
Abstract: Epistemic updating is the
process of changing multi-agent epistemic situations (multi-agent Kripke
models) by means of informative communicative acts, such as public
announcements, group messages, private messages, and so on. We propose to use an
epistemic version of propositional dynamic logic (PDL) for this. First we
sketch how epistemic PDL can be used to model epistemic situations, including
the description of what is common knowledge among groups of agents. Next, we
show how epistemic update PDL (PDL with update actions) can be translated to
epistemic PDL. This translation yields a sound and complete proof system for
epistemic update PDL, and it can be used to find appropriate axioms for
special cases of updates. We end with a brief
demonstration of DEMO, a tool for Dynamic Epistemic Modelling (modelling
epistemic updates, graphical display of update results, graphical display of
action models, formula evaluation in epistemic models, translation of
epistemic update formulas to epistemic PDL formulas, and so on). References: http://www.win.tue.nl/zic/doc/JvEijck.bib |
|
Date: |
|
|
Title: |
Incompleteness Proof in Coq |
|
Speaker(s): |
Russell O'Connor |
|
Abstract: In this talk I will present
my formalization of the Goedel-Rosser Incompleteness Theorem in Coq. I will
discuss the approach taken, and how it differs from the previous
formalization of the Incompleteness theorem. I will also discuss my
experiences using Coq and the difficulties I encountered when learning to use
the proof system. The audience should be
familiar with dependent type theory and inductive data structures. It would
be useful to know a bit about Coq, or at least how dependent type theory is
used to represent proofs. |
|
Date: |
|
|
Title: |
The type system of Axiom |
|
Speaker(s): |
Note: joint work with Simon Thompson at the
University of Kent at Canterbury
|
Abstract: The computer algebra system Axiom is
unusual among computer algebra systems because it is strongly typed. I'll
discuss the type system of Aldor, which is the programming language of Axiom,
and discuss how this might be used to combine computer algebra and theorem
proving by exploiting the Curry-Howard-de Bruijn isomorphism. |
|
Date: |
|
|
Title: |
IF-logic from a game-theoretical perspective |
|
Speaker(s): |
|
Abstract: Game Theoretical Semantics
is an alternative to Tarski semantics on first order predicate logic, that
adapts easily to extensions of first order logic. A notable example is
Hintikka's "Independence Friendly Logic", IF-logic for short, which
allows for more general dependence patterns between quantifiers. These
patterns can be interpreted by switching from games of perfect information to
games of imperfect information in the semantics. In this talk, I will show
some connections between results and concepts from the theory of games of
imperfect information, and logical properties of IF-logic. In particular, I
show how logical equivalence schemes in IF-logic can be seen to correspond to
the so-called Thompson transformations on games of imperfect information. We
also see the evaluation of some surprising and debated IF-formulas in the
light of the game theoretic concept of "imperfect recall", the interpretation
of which is a topic of debate in game theory. These examples give us some
appealing correspondences between IF-logic and game theory, but I will argue
that they also reveil that the class of IF-semantic games is
game-theoretically rather unnatural. |
|
Date: |
|
|
Title: |
Weak bisimulation for action-type coalgebras |
|
Speaker(s): |
Note: joint work with Erik de Vink and Harald Woracek
|
Abstract: We propose a coalgebraic definition of
weak bisimulation for a class of coalgebras obtained from bifunctors over the
category SET. Weak bisimilarity for a system is obtained as strong
bisimilarity of a transformed system. The transformation consists of two
steps: First, the behaviour on actions is expanded to behaviour on finite
words. Second, the behaviour on finite words is taken modulo the hiding of
invisible actions, yielding behaviour on equivalence classes of words closed
under silent steps. The coalgebraic definition is justified by two
correspondence results, one for the classical notion of weak bisimulation of
Milner and another for the notion of weak bisimulation for generative
probabilistic transition systems as advocated by Baier and Hermanns. |
|
Date: |
|
|
Title: |
A stepwise approach to formalizing mathematics |
|
Speaker(s): |
Note: Please note that the ZIC will be in a DIFFERENT
ROOM than usual.
|
Abstract: In this talk I present ongoing work on
studying the process of creating a fully formalized and computer-checked
document from a piece of informal mathematics. Our approach, based on Weak
Type Theory (WTT), allows the definition of several stages of this process,
each with increasingly stronger correctness requirements. Every one of these
stages presents opportunities for computer assistance and checks that help
the developer of the formal text and guarantees higher level of reliability
of the formalization as a whole. I will discuss both the general setting and
goals of the project as well as some recent ongoing work on the automatic
translation of a segment of WTT into type theory with open terms. |
|
Date: |
|
|
Title: |
Deciding static properties of XPath expressions |
|
Speaker(s): |
|
Abstract: In the first part of this
talk we discuss the problem of finding a sound and complete rule set for
determining whether sorting and duplicate removal operations in the query
plan of XPath expressions are unnecessary. Additionally we define a
deterministic infinite automaton that illustrates how these rules can be
translated into an efficient algorithm. This work is an important first step
in the understanding and tackling of XPath/XQuery optimization problems that
are related to ordering and duplicate removal. In the second part of this
talk we investigate the complexity of deciding the satisfiability of XPath
2.0 expressions, i.e., whether there is an XML document for which their
result is nonempty. Several fragments that allow certain types of expressions
are classified as either in PTIME or NP-hard to see which type of expression
make this a hard problem. Finally, we establish a link between XPath
expressions and partial tree descriptions which are studied in computational
linguistics. |
|
Date: |
|
|
Title: |
Equivalences for silent transitions in Probabilistic
Systems |
|
Speaker(s): |
Suzana Andova |
|
Abstract: We address abstraction in the setting
of probabilistic reactive systems, and study its formal underpinnings for the
strictly alternating model. In particular, we define the notion of branching
bisimilarity and study its properties by studying two other equivalence
relations, viz.\ coloured trace equivalence and branching bisimilarity using
maximal probabilities. We show that both alternatives coincide with branching
bisimilarity. The alternative characterisations have their own merits and
focus on different aspects of branching bisimilarity. Together they give a
better understanding of branching bisimilarity. Furthermore, we show that the
notions of branching bisimilarity in the alternating and in the non-alternating
model differ, and that the latter one discriminates between systems that are
intuitively branching bisimilar. |
|
Date: |
|
|
Title: |
Derivability and admissibility of inference rules in
abstract Hilbert systems |
|
Speaker(s): |
|
Abstract: In this talk I will broadly
follow a recent report with the same title. The aim there was to collect
general results about the notions of derivability and admissibility that
apply to all Hilbert-style proof systems ``of simplest kind''. For this purpose, a general
framework for Hilbert systems is introduced in which it is abstracted from
the syntax of formulas and the operational content of rules. In these ``abstract
Hilbert systems'' (AHS's) a rule is a set of inference steps that is endowed
with a premise and a conclusion function. Subsequently the notions of rule
derivability and admissibility are adapted to AHS's, two variants of rule
derivability are proposed, and the relationships of these four notions
towards each other are investigated. In a further step,
relations are considered that compare AHS's with respect to rule
admissibility, a notion of rule derivability, or a particular consequence
relation. A theorem is given that captures the relationships towards each
other of 24 such relations. And eventually, the question is explored of what
consequences the property of a rule R to be derivable or admissible in an AHS
S does entail for the possibility to eliminate applications of R from
derivations in the extension of S by adding R. Links: |
|
Date: |
|
|
Title: |
Tool support for developing JML specs |
|
Speaker(s): |
Note: Please note that the ZIC will be in a DIFFERENT
ROOM than usual.
|
Abstract: The specification language
JML (www.jmlspecs.org) is becoming the de facto standard for writing
specifications for Java programs. JML is easy to use for Java programmers
since its syntax stays close to Java. Moreover, JML is supported by many
tools, which help to check a specification with respect to an implementation. In the past, we've applied
JML to many Java and Java Card case studies. One of the lessons we learned is
that coming up with good JML specifications is often the hardest part of
verifying a given implementation. This talk gives a short
overview of JML and its application to Java Card. Some of the existing tools
are discussed, as well as current work on tools that should make life easier
for people developing JML specifications. |
|
Date: |
|
|
Title: |
Automath Symposium |
|
Speaker(s): |
|
|
Abstract: A joint symposium with the
seminar of the Foundations Group in Nijmegen and the ZIC Colloquium on the
occasion of the digitalization of the Automath Archive |
|
Date: |
|
|
Title: |
Interpreting descriptions in intensional type theory |
|
Speaker(s): |
Jesper Carlström (Stockholm, Nijmegen) |
|
Abstract: We give calculi for
intuitionistic first order logic with indefinite and definite descriptions
(choice-operators for full choice and unique choice, respectively) and
interpret these calculi in Martin-Löf's intensional type theory. A
substantial part of mathematics can be naturally expressed in first order
logic with descriptions; and hence it can be understood intensionally via the
interpretation. |
|
Date: |
|
|
Title: |
Cut elimination for axiomatic theories |
|
Speaker(s): |
Gilles Dowek (France) |
|
Abstract: Gentzen cut elimination
theorem for predicate logic is a central result in proof theory allowing to
prove the consistency of deduction, independence results, the disjunction and
the witness property for constructive proofs, the completeness of proof search
methods, decidability of fragments, ... However, most of these
results cannot be derived from the cut elimination theorem anymore when we
consider deduction in an axiomatic theory, and some extensions of the cut
elimination theorem are needed to obtain similar results for theories such as
arithmetic and type theory. In this seminar, I will
present recent work towards a notion of cut elimination for axiomatic
theories. The main interest of these developments is that they challenge the
notion of axiomatic theory and show the way to the more computational
oriented notion of theory. |
|
Date: |
|
|
Title: |
Formalizing Constructive Mathematics in Type Theory |
|
Speaker(s): |
Luís Cruz-Filipe |
|
Abstract: In this talk I will present
C-CoRN, the Constructive Coq Repository at Nijmegen. As its name suggests,
C-CoRN is a library of formalized constructive mathematics developed in the
theorem prover Coq. In what way and for what purposes such a library can be developed
and used will be the main topics of the presentation. One of the basic
definitions in C-CoRN is that of partial function. will discuss and compare
several different ways in which partial functions can be represented both in
Coq and in other type theories. As an example of the use of this definition,
I will show how the usual functions of analysis (sine, exponential,
logarithm) can be defined and used. Another aspect of C-CoRN is
automation of proofs. I will explain how equational reasoning can be done
without user intervention and show how this hugely simplifies proofs. Finally, I will pursue the
possible applications of C-CoRN with an overview of program extraction and
how, in theory, the formalization of the Fundamental Theorem of Algebra could
be used to obtain a root-finding program. Unfortunately, as will be seen, the
theory and the practice do not coincide. |
|
Date: |
|
|
Title: |
A Brief History of Process Algebra |
|
Speaker(s): |
Jos Baeten |
|
Abstract: This talk addresses the
history of process algebra as an area of research in concurrency theory, the
theory of parallel and distributed systems in computer science. Origins are
traced back to the early seventies of the twentieth century, and developments
since that time are sketched. The speaker gives his personal views on these
matters. He also considers the present situation, and states some challenges
for the future. |
|
Date: |
|
|
Title: |
A Calculus of Tactics and Its Operational Semantics |
|
Speaker(s): |
Georgi Jojgov |
|
Abstract: In interactive theorem
proving one uses a computer program called 'proof assistant' to create proofs
and develop theories. The proof assistant does the bookkeeping and automates
certain tasks and the human provides guidance. The commands for creating
proofs provided by the proof assistant are usually called 'tactics'. In this
talk we will discuss a calculus that is capable of describing some common
tactics in theorem provers based on type theory. The calculus is an extension
of a calculus of open terms with proof-search primitives as unification
constraints, recursion, exception handling, etc. We will present typed
operational semantics for the calculus and show some of its properties. |
|
Date: |
|
|
Title: |
Shannon information and Kolmogorov Complexity |
|
Speaker(s): |
Peter Grünwald |
Note: The article of Peter Grünwald and Paul Vitányi,
on the subject of Shannon information and Kolmogorov Complexity (Journal of
Logic, Language and Information (12), pp.497-529, 2003), is available at Peter's publication webpage.
|
Abstract: We introduce, compare and
contrast the theories of Shannon information and Kolmogorov complexity.
Roughly speaking, the former measures information relative to random
variables, defined relative to some known probability distribution. The
latter measures information in individual objects (sequences of symbols or
numbers), and makes no probabilistic assumptions. We investigate the extent
to which these theories have a common purpose and where they are
fundamentally different. We discuss the fundamental relations `entropy =
expected Kolmogorov complexity' and `Shannon mutual information = expected
algorithmic information'. We show how `universal coding/modeling' (a central
idea in practical data compression) may be viewed as a middle-ground between
the two theories, and how it leads to the 'minimum description length
principle', a practically useable theory for statistical inference with
arbitarily complex models. |
|
Date: |
|
|
Title: |
Partial orders make monads even more useful |
|
Speaker(s): |
Patrik Eklund (Finland) |
Note: presentation (pdf)
|
Abstract: Composing various powerset
functors with the term monad gives rise to the concept of generalised terms.
The goal is to extend traditional term unification with unification involving
powersets of terms. This enables a study of substitutions and unifiers within
Kleisli categories related to particular monads. As constructions of monads
involve complicated calculations with natural transformations, proofs are
supported by a graphical approach that provides a useful tool for handling
various conditions, such as those for distributive laws. Monads equipped with order
structures extends suitably to so called partially ordered monads. We will
show how these partially ordered monads, together with their
subconstructions, contribute to providing a generalised notion of powerset
Kleene algebras. This generalisation builds upon more general powerset
functor setting far beyond just strings (Kleene, 1956) and relations (Tarski,
1941). |
|
Date: |
|
|
Title: |
Logic in equilibrium and equilibrium in logic |
|
Speaker(s): |
Paul Harrenstein |
|
Abstract: Von Neumann and Morgenstern
presented game-theory as a branch of mathematics that deals with problems
that had nowhere been dealt with before. From a mathematical point of view,
the participants in a situation of conflict can be seen as each trying to maximize
the same function (the outcome of the game) according to an idiosyncratic
principle (their preferences). Moreover, none of the players have control
over all variables of the function. The also argued that the usual notion of
optimality is no longer available and new solution concepts had to be
developed to take its place. Most notably among these game-theoretical
solution concepts is still that of a Nash-equilibirum. In this presentation we
explore two different ways in which the notion of Nash-equilibrium can be
approached from a logical angle. First, we propose a
multi-modal propositional logic, which is is designed to describe and reason
about games in extensive form. The concept of a (subgame perfect) Nash
equilibrium| can be characterized by a formula scheme. We also present a
completeness result for this logic. Logical notions of
consequence have frequently been related to game-theoretical solution
concepts. The correspondence between a formula being classically valid and
the existence of a winning strategy for a player in a related two-person
game, has been most prominent in this context. In the second part of this
talk, however, we propose a conservative extension of the classical notion of
consequence for propositional logic based on a generalization of
Nash-equilibrium. We construe propositional variables as decision variables
that are possibly in the control of various agents and pursue the logical
consequences of this idea. The game-theoretical concept of consequence that
results opens up a line of theoretical research in which logic, game theory
and social choice theory interact at the same level. |
|
Date: |
|
|
Title: |
Discrete-time rewards model-checked |
|
Speaker(s): |
Suzana Andova |
|
Abstract: A model-checking approach
for analyzing discrete-time Markov reward models is presented. For this
purpose, the temporal logic probabilistic CTL is extended with reward
constraints. This allows to formulate
complex measures - involving expected as well as accumulated rewards - in a
precise and succinct way. Algorithms to efficiently analyze such formulae are
introduced. The approach is illustrated by model-checking a probabilistic
cost model of the IPv4 zeroconf protocol for distributed address assignment in
ad-hoc networks. |
|
Date: |
|
|
Title: |
Unique Decomposition |
|
Speaker(s): |
Bas Luttik |
|
Abstract: An element of a commutative
monoid is indecomposable if it is not the composition of two elements that
are both not the identity element of the monoid. A commutative monoid has
unique decomposition if every element can be uniquely expressed as the
composition of indecomposable elements. The best known example of a commutative
monoid with unique decomposition is the set of positive natural numbers with
multiplication as composition (and the prime numbers as indecomposable
elements). We introduce the notion of
decomposition order for arbitrary commutative monoids. Our main result is
that a commutative monoid has unique decomposition if, and only if, it can be
equipped with a decomposition order. We shall indicate how our
result can be used to establish unique decomposition for 1. the commutative
monoid of natural numbers with addition; 2. the commutative monoid of
positive natural numbers with multiplication; and 3. the commutative monoid
of weakly normed ACP_epsilon expressions with parallel composition (assuming
handshaking communication). If time permits we shall
also indicate how our result can be generalised to partial commutative
monoids (i.e., in which composition is a partial operation) so that it
applies to (the partial commutative monoids associated with) well-founded
Commutative Residual Algebras. Joint work with Vincent van
Oostrom (UU). |
|
Date: |
|
|
Title: |
Individual Choice Sequences in the work of Brouwer |
|
Speaker(s): |
Joop Niekus (UvA) |
|
Abstract: Choice sequences are
sequences not completely determined by a law. We state that the introduction
of particular choice sequences by Brouwer in the late twenties was not
recognised as such. We claim that their later use in the method of the
creative subject was not traced back to this original use of them and has
been misinterpreted. We show where these particular choice sequences appear
in the work of Brouwer and we show how they should be handled. |
|
Date: |
|
|
Title: |
Concise Graphs and Functional Bisimulations |
|
Speaker(s): |
Ling Cheung (KUN) |
|
Abstract: It is well-known that
bisimilarity between two processes P and Q can be characterized by the
existence of another process R and functional bisimulations from R to P and
from R to Q. In fact, any bisimulation relation R between P and Q can be made
into a process in such a way that the projections are functional
bisimulations. Our work is largely
motivated by the following question: when does there exist a smallest such
process R? In particular, if one adopts the approach of "bisimulations
as processes", how can one guarantee the existence of least
bisimulations (under set inclusion)? In this talk, we introduce
concise process graphs and prove existence of the least bisimulation between
a concise graph and any other bisimilar graph. This definition has many
consequences, among which existence of binary products and coproducts in the
category P of process graphs and functional bisimulations. Moreover, the
subcategory CP of concise graphs is coreflective in P. We close by asking:
"Is conciseness useful in any way?" and "How can conciseness
be adapted to a setting with silent steps?" |
|
Date: |
|
|
Title: |
A hierarchy of probabilistic system types |
|
Speaker(s): |
Ana Sokolova (TU/e) and Falk Bartels (CWI) |
Note: (Joint work with Erik de Vink (TU/e))
|
Abstract: Many approaches in standard
concurrency theory are commonly based on labelled transition systems or some
minor variant thereof. When probabilities are introduced however, many
different system types emerge: some authors for instance consider fully
probabilistic systems, while others use systems which incorporate both,
nondeterministic and probabilistic choice. In the latter case, various
restrictions are furthermore imposed about when or in which order nondeterministic
and probabilistic steps are allowed and which of them are associated with
input or output labels. We survey the different
probabilistic models in use and arrange them in an expressiveness hierarchy.
To this end a coalgebraic presentation turns out to be appropriate not only
to describe the various systems with their associated notion of bisimilarity,
but also to define translations of one type into another. Moreover, we
present a simple sufficient criterion for such a translation to preserve
expressiveness. |
|
Date: |
|
|
Title: |
Constructive and Computer mathematics |
|
Speaker(s): |
Bas Spitters (KUN) |
|
Abstract: In this talk I will
highlight two views on constructive mathematics: 1) as an abstract theory of
computation and 2) as an abstract programming language. 1. Constructive logic can
be seen to be the "internal" logic for several models of
computations. For instance, Turing machines models or so-called type-2 Turing
machines models. I will illustrate the two approaches by looking at
computations on the real numbers. 2. Constructive mathematics
can be formalized in type theory and as such it is a very abstract
programming language. This formalization can be done with the aid of a computer.
I will give a short description of the formalization of a part of
constructive mathematics in the Coq proof assistent by the Foundations group
in Nijmegen. Finally, I will say a few words about experiments with the
extraction of useful programs from such formalizations. |
|
Date: |
|
|
Title: |
Tableaux for Quantified Hybrid Logic |
|
Speaker(s): |
Maarten Marx
(UvA) |
Note: Full paper (pdf) with
Patrick Blackburn (INRIA) slides
(ps)
|
Abstract: We present a (sound and
complete) tableau calculus for Quantified Hybrid Logic (QHL). QHL is an
extension of orthodox quantified modal logic: as well as the usual Box- and Diamond
modalities it contains names for (and variables over) states, operators @_s
for asserting that a formula holds at a named state, and a binder
$\downarrow$ that binds a variable to the current state. The first-order
component contains equality and rigid and non-rigid designators. As far as we
are aware, ours is the first tableau system for QHL. Completeness is established
via a variant of the standard translation to first-order logic. More
concretely, a valid QHL-sentence is translated into a valid first-order
sentence in the correspondence language. As it is valid, there exists a
first-order tableau proof for it. This tableau proof is then converted into a
QHL-tableau proof for the original sentence. In this way we recycle a
well-known result (completeness of first-order logic) instead of a well-known
proof. The tableau calculus is
highly flexible. We only present it for the constant domain semantics, but
slight changes render it complete for varying, expanding or contracting
domains. Moreover, completeness with respect to specific frame classes can be
obtained simply by adding extra rules or axioms (this can be done for every
first-order definable class of frames which is closed under and reflects
generated subframes). |
|
Date: |
|
|
Title: |
Probabilistic Dynamic Epistemic Logic |
|
Speaker(s): |
Barteld Kooi
(RUG) |
|
Abstract: My talk is about
probabilistic dynamic epistemic logic, a logic for reasoning about
probability, information, and information change. Epistemic logic is a modal
logic used to reason about information. This may also contain information
about the information of other agents, because epistemic logic is suited to
deal with situations involving more than one agent. In this way epistemic
logic also deals with higher order information, i.e. information about
information. Although epistemic logic
provides good means of analysis of higher order information, it does not
involve information change. Dynamic epistemic logics are extensions of
epistemic logic that can deal with information change. It is interesting to
note that both in dynamic epistemic logic and in probability theory
incorporating new information is studied. In probability theory this is done
by taking conditional probabilities, also known as Bayesian updating. The
crucial difference between the two approaches is due to a difference in
perspective on information change: in dynamic epistemic logic learning that
something is the case can change the truth value of some propositions. In
probability theory this is assumed not to be the case. This difference in
perspective becomes apparent when you are interested in higher order
information. The question that pops up is what these two fields could learn
from each other with respect to information change. I think that probability
theory could greatly benefit from the theory of information change provided
by dynamic epistemic logic. In my talk I present a
probabilistic dynamic epistemic logic that provides a novel approach to
probabilistic updating, because it does take higher order information into
account. |
|
Date: |
|
|
Title: |
The context cube: the lambda cube with contexts |
|
Speaker(s): |
Mirna Bognar (Deloitte & Touche, previous
affiliation: VU) |
|
Abstract: We present the context cube
$\lambda []$, a system of eight context calculi corresponding to Barendregt's
lambda cube with contexts. In the context cube, the expressions and
meta-contexts of the lambda cube can be represented. Moreover, filling of the
holes of a context is a rewrite relation. The novelty of the context
cube is that it also deals with contexts with dependent types. The simplicity
of the context cube lies in the fact that it can be translated into the
lambda cube. Rewriting in the context cube is confluent and strongly
normalising. Furthermore, we illustrate
how a mathematical structure can be representated as a context within the
context cube, in such a way that it can be used, for example, in proofs. Our
representations are basically de Bruijn's segments, but with holes in types
to obtain a uniform representation. |
|
Date: |
|
|
Title: |
"adbmaL" |
|
Speaker(s): |
Vincent van
Oostrom and Dimitri Hendriks (UU) |
|
Abstract: Slides available at http://www.phil.uu.nl/~oostrom/publication/rewriting.html.
|
|
Date: |
|
|
Title: |
Reachability Analysis of Probabilistic Systems by
Successive Refinements |
|
Speaker(s): |
Pedro d'Argenio (Universidad Nacional de Cordoba,
Argentina) |
|
Abstract: The last few years
witnessed a continuosly growing interest in Quantitative Model Checking, that
is, model checking in which the truth of a property is quantified by a
probabilistic value. This talk will focus on a novel development to model
check quantitative reachability properties on Markov decision processes
together with its prototype implementation. The innovation of the technique
is that the analysis is performed on an abstraction of the model under
analysis. Such an abstraction is significantly smaller than the original
model and may safely refute or accept the required property. Otherwise, the
abstraction is refined and the process repeated. As the numerical analysis
necessary to determine the validity of the property on the concrete Markov
decision processes is more costly than the refinement process, the technique
profits from applying such numerical analysis on smaller state spaces. |
|
Date: |
|
|
Title: |
A constraint based system for the verification of
security protocols |
|
Speaker(s): |
Sandro Etalle (Twente University) |
|
Abstract: In [1] we propose a
constraint-based system for the verification of security protocols. Our
system is an improvement on that of Millen and Shmatikov and features (1) a
new semantics, that lead to a significantly more efficient implementation,
(2) a monotonic behavior, which also allows to detect flaws associated to
partial runs and (3) a more expressive syntax, in which a principal may also
perform explicit checks. In this paper we also show why these improvements
yield a more effective and practical system. This talk is meant as a
(smooth) introduction to the system of [1] and to the use of
constraint-solving for the verification of security protocols. [1] R. Corin and S. Etalle.
An Improved Constraint-Based System for the Verification of Security
Protocols. Proc. 2002 Static Analysis Symposium. Springer-Verlag,
LNCS, 2002. To
appear. |
|
Date: |
|
|
Title: |
Towards the Formal Verification of Social Mechanisms |
|
Speaker(s): |
Marc Pauly (University of Liverpool) |
|
Abstract: Game theory and logic can
provide the tools for a more formal analysis of the social mechanisms we are
involved in, such as voting procedures, auctions, and negotiation. After
spending some time to motivate this research program in general, I will focus
on a particular technical example, an extension of the WHILE-language for
programming game-theoretic mechanisms involving multiple agents. A structured
operational semantics is provided in terms of extensive games of almost
perfect information. Hoare-style partial correctness assertions are proposed
to reason about the correctness of these mechanisms, where correctness is
interpreted as the existence of a subgame perfect equilibrium. Using an
extensional approach to pre- and postconditions, we show that an extension of
Hoare's original calculus is sound and complete for reasoning about subgame
perfect equilibria in game-theoretic mechanisms. |
|
Date: |
|
|
Title: |
The Coinductive Approach to Verifying Cryptographic
Protocols |
|
Speaker(s): |
Jesse Hughes (KUN) |
|
Abstract: We look at a new way of
specifying and verifying cryptographic protocols using the Coalgebraic Class
Specification Language (CCSL). Our approach starts by providing a CCSL
specification which models a cryptographic protocol (and inherits from a more
abstract class specification). We include with the specification the
correctness conditions to be proved (representing, typically, secrecy and
authentication). This specification is compiled into a number of PVS
theories. The correctness theorems are then proven within PVS, using a
temporal logic derived from the coalgebraic specification of the protocol. We
will conclude with a comparison with other approaches for analyzing
cryptographic protocols. The main distinguishing feature of our approach is
that it takes coalgebraic theory as its foundation. |
|
Date: |
|
|
Title: |
Smartcard security: Attacking the implementation. |
|
Speaker(s): |
Jerry den Hartog |
|
Abstract: The security properties of
cryptographic algorithms run on smartcards are usually well understood. The
implementation of the algorithm on a smartcard, however, may provide an
attacker with additional information which is assumed to remain secret in the
analysis of the security of the algorithm. Simply measuring the amount of power
used by the smartcard during execution, for example, can provide information
about the data that is being manipulated. This presentation discusses a tool
that is being developed to analyze the risk of power analysis attack and
other so called side channel attacks on the implementation of cryptographic
algorithms on a smart card. The tool is illustrated by simulating a power
analysis attack on a simple enciphering algorithm. |
|
Date: |
|
|
Title: |
Formal Verification of a Simple Java Card Payment
Applet |
|
Speaker(s): |
Martijn
Oostdijk (KUN) |
|
Abstract: In this talk we discuss
some recent work on the formal verification of smart card payment
implementations. We present an extremely simple Java Card applet whose
specification can be formulated as "the Applet's balance field can only
be decreased, never increased". We demonstrate how the implementation
can be formally shown to be correct using the specification language JML and
the Loop tool. We then extend this applet with a challenge-response mechanism
which allows trusted terminals to increase the balance. This complicates
things. However, some very useful properties of the extended applet can still
be specified in JML and formally checked. Joint work with B. Jacobs and M.
Warnier. |
|
Date: |
|
|
Title: |
Logic and game theory: Hintikka's Independence Friendly
Logic |
|
Speaker(s): |
Francien Dechesne |
|
Abstract: My talk will start with an
overview of Independence Friendly logic (IF-logic) as introduced by Hintikka
in his book `The Principles of Mathematics Revisited' (1996). The syntax for
IF-logic is an extension of the formalism for classical first order predicate
logic. By a slash notation, we can make a quantifier or connective
independent of a quantifier in whose scope it occurs. An IF-sentence gets its
interpretation from Game Theoretical Semantics (GTS): truth and falsity of a
sentence in a given model are defined in terms of the existence of winning
strategies for the players in the associated 2-player semantical game. On
first order sentences, Tarskian semantics and GTS coincide. The slash
notation results in semantical games of imperfect information, which are in
general not determined. Central in GTS is the notion of strategy. In the
tradition of the theory of branching quantification (Henkin, 1960's),
Hintikka formulates the existence of winning strategies in terms of Skolem
functions. I will show how the semantical games can be formalized in a
standard game theoretical framework. It shows that Skolem functions yield a
significant restriction of the standard game theoretical notion of strategy. |