TSSS 2012-2

Date: 15:00-16:00, Feb. 15 (Wed), 2012
Place:  Room SB-1001 (Sogo-Kenkyuto-B, 10th Floor)

Speaker: Chung-chieh (Ken) Shan
Title: Embedding probabilistic languages

Abstract:
Probabilistic inference is popular in machine learning for writing
programs that classify music and locate planes.  It is also useful in
cognitive science for modeling how people interpret words and recognize
faces.  However, it is applied much less than it could be because
most inference programs are written from scratch by hand.  Instead,
probabilistic models and inference procedures should be written as
separate reusable modules.  To this end, we carried out and popularized
a new approach that is easier to use and more expressive, namely to
write models and inference in the same general-purpose language.  Our
approach makes deterministic parts of models run at full speed and
lets inference procedures reason about themselves without interpretive
overhead.  I will describe our approach and how we apply the same
inference implementations to multiple realistic models, with performance
competitive with the state of the art.  This work exemplifies a
recurring theme: we can apply tools from programming-language theory,
such as continuations and staging, to represent declarative knowledge as
executable code instead of passive data.

Dr. Chung-chieh Shan's web page is
  http://www.cs.ruters.edu/~ccshan/ 

TSSS 2012-1

Date & Time: February 7, 2012, 11:00 - 12:00
Venue : SB 110, University of Tsukuba

Speaker: Olga Caprotti 
         Department of Computer Science and Engineering,
         Chalmers University of Technology and University of Gothenburg, Sweden

Title: MOLTO, Multilingual Online Translation

Abstract MOLTO's goal is to develop a set of tools for translating
texts between multiple languages in real time with high
quality. Languages are separate modules in the tool and can be varied;
prototypes covering a majority of the EU's 23 official languages will
be built.  As its main technique, MOLTO uses domain-specific semantic
grammars and ontology-based interlinguas. These components are
implemented in GF (Grammatical Framework), which is a grammar
formalism where multiple languages are related by a common abstract
syntax. GF has been applied in several small-to-medium size domains,
typically targeting up to ten languages but MOLTO will scale this up
in terms of productivity and applicability.

A part of the scale-up is to increase the size of domains and the
number of languages. A more substantial part is to make the technology
accessible for domain experts without GF expertise and minimize the
effort needed for building a translator. Ideally, this can be done by
just extending a lexicon and writing a set of example sentences.

The most research-intensive parts of MOLTO are the two-way
interoperability between ontology standards (OWL) and GF grammars, and
the extension of rule-based translation by statistical methods. The
OWL-GF interoperability will enable multilingual
natural-language-based interaction with machine-readable
knowledge. The statistical methods will add robustness to the system
when desired. New methods will be developed for combining GF grammars
with statistical translation, to the benefit of both.

MOLTO technology will be released as open-source libraries which can
be plugged in to standard translation tools and web pages and thereby
fit into standard workflows. It will be demonstrated in web-based
demos and applied in three case studies: mathematical exercises in 15
languages, patent data in at least 3 languages, and museum object
descriptions in 15 languages.

TSSS 2011-3

Date: 16:00-17:00, Jan 12, 2012

Place: Room SB-1111

Speaker: Jun Inoue (Department of Computer Science, Rice University)

Title: Reasoning About Multi-stage Programs
       (The talk will be given in Japanese.)

Abstract:

Multi-stage programming (MSP) is a style of writing program
generators---programs which generate programs---supported by special
annotations that direct construction, combination, and execution of
object programs.  Various authors have shown MSP to be effective in
writing efficient programs without sacrificing genericity.  However,
correctness proofs of such programs have so far received limited
attention, and approaches and challenges for that task have been
largely unknown.  In this thesis, I establish formal equational
properties of the multi-stage lambda calculus and related proof
techniques, as well as results that delineate the intricacies of
multi-stage languages that one must be aware of.

In particular, I settle three basic questions that naturally arise
when verifying multi-stage functional programs.  Firstly, can adding
staging MSP to a language compromise the interchangeability of terms
that held in the original language?  Unfortunately it can, and more
care is needed to reason about terms with free variables.  Secondly,
staging annotations, as the name ``annotations'' suggests, are often
thought to be orthogonal to the behavior of a program, but when is
this formally guaranteed to be the case?  I give termination
conditions that characterize when this guarantee holds.  Finally, do
multi-stage languages satisfy extensional facts, for example that
functions agreeing on all arguments are equivalent?  I develop a
sound and complete notion of applicative bisimulation, which can
establish not only extensionality but, in principle, any other valid
program equivalence as well.  These results improve our general
understanding of staging and enable us to prove the correctness of
complicated multi-stage programs.

TSSS 2011-2

Date: 14:00-16:00, Dec 15, 2011

Place: Room SB-1112

1. Kohei Suenaga (Kyoto University, JSPS Research Fellow (PD))
   Programming with Infinitesimals: A WHILE-Language for Hybrid System Modeling 
   (Joint work with Ichiro Hasuo) 
2. Keiko Nakata (Institute of Cybernetics, Tallinn University of Technology)
   Hoare Logic for the Coinductive Trace-Based Big-Step Semantics of While
   (Joint work with Tarmo Uustalu.) 

Abstracts:

1. Programming with Infinitesimals: A WHILE-Language for Hybrid System Modeling  

We add, to the common combination of a WHILE-language and a
Hoare-style program logic, a constant dt that represents an
infinitesimal (i.e. infinitely small) value.
The outcome is a framework for modeling and verification
of hybrid systems: hybrid systems exhibit both continuous and discrete dynamics
and getting them right is a pressing challenge. We rigorously define
the semantics
of programs in the language of nonstandard analysis, on the basis of which the
program logic is shown to be sound and relatively complete.

2. Hoare Logic for the Coinductive Trace-Based Big-Step Semantics of While

In search for a foundational framework for reasoning about observable
behavior of programs that may not terminate, we have previously
devised a coinductive operational semantics for While.  The
operational semantics keeps track of all the states that an execution
goes through as a trace (a possibly infinite sequence of states). The
trace is finite for a terminating execution and infinite for a
non-terminating execution.  Subsequently we designed a Hoare logic
counterpart of our coinductive trace-based semantics and proved it
sound and complete. Our logic subsumes both the partial
correctness Hoare logic and the total correctness Hoare logic: they
are embeddible.

All the results have been formalized in Coq constructively.

In this talk, I will overview the coinductive operational semantics
and the Hoare logic, aiming at delivering the intuition behind.

(Joint work with Tarmo Uustalu.)

TSSS 2011-1

Date: 14:00-15:00, Mar 14, 2011

Place: Room SB-1001

Speaker: Marcin Paprzycki, Systems Research Institute of the Polish Academy of Sciences 

Title: Introduction to Software Agents and their Applications

Abstract:

Since 1994 we are told that software agents will become the next revolution
in computing [3]. This change is to occur not only in the ways we construct
software [2] but also to profoundly impact human-computer interactions [1,
3]. Unfortunately, when we turn the computer on in the morning, we do not
contact our Personal Agent to receive a personalized newscast, our day-plan
and, on the basis of that plan as well as the weather forecast and knowledge
of our dressing-preferences, an advice what to wear. Similarly, when
creating software for an e-shop we do not utilize pre-existing agent-modules
(e.g. advertising agents, seller, inventory manager, etc.). Instead, there
exist only few successful large-scale implementations of agent systems.

In the seminar, a general introduction to software agents will be presented.
Discussion includes topics like: conceptual roots and definition of software
agents and agent systems, major points raised “for” and “against” software
agent systems, existing applications of agent systems, and possibility of
developing large scale agent systems. No previous exposure to software
agents and agent systems is assumed.

*References*

1.  J. Hendler, Is There an Intelligent Agent in Your Future?, Nature, 11,March, 1999

2.  N. R. Jennings, An agent-based approach for building complex software systems, 
    CACM, 44 (4), 2001, 35-41

3.  P. Maes, Agents that Reduce Work and Information Overload, Communications of the ACM, 37(7), 
    1994, 31-40

TSSS 2010-5

Date: September 17, 2010

Place: Room SB-1001

Program:

13:00 - 14:00
Verifying floating-point algorithms using formalized mathematics
John Harrison (Intel Corporation, USA)
Abstract

14:15 - 14:45
Translating Regular Expression Matching into Transducers
Yasuhiko Minamide (University of Tsukuba)
 (joint work with Yuto Sakuma and Andrei Voronkov)

14:45- 15:15
General bindings in Nominal Isabelle
Cezary Kaliszyk (University of Tsukuba)

15:15 - 15:45
Proof certificate for origami theorem proving
Tetsuo Ida (University of Tsukuba)

16:00 - 16:30
Modules for Origami Constructions
Fadoua Ghourabi (University of Tsukuba)

16:30 - 17:00
Web Origami System: WebEos
Asem Kasem (University of Tsukuba)

TSSS 2010-4

Date: 10:00-11:30, Sep 2, 2010

Place: Room SB-1001

Speaker: Cezary Kaliszyk, University of Tsukuba 

Title: Computer Algebra and Proof Assistants

Abstract:

Computer algebra systems are programs that allow manipulation
and processing of mathematical expressions. However, the algorithms
provided are not formally verified, which makes computer
algebra systems less reliable than proof assistants.

In this talk we present an approach which bridges the gap
between the two classes of systems. We show a computer
algebra system that ensures absolute correctness of performed
simplifications by using the decision procedures present in
a proof assistant. We show how the system can be extended with
an approach for treating partiality and effective computation with
real numbers.

TSSS 2010-3

Workshop on Symbolic Computation and Software Verification
 Date: Apr 8-9, 2010
Link

TSSS 2010-2

Date: 15:00-17:00, Mar 26, 2010

Place: Room SB-1001
 Date: 15:00-17:00, Mar 24, 2010

Place: Room SB-1112
 
Speaker: Andreiv Voronkov, University of Manchester
 Title: Tutorial on on satisfiability and theories/SMT 
 

TSSS 2010-1

Date: 11:00-, Mar 11, 2010

Place: Room SB-1001

Speaker: Keiko Nakata, Institute of Cybernetics, Tallinn University of Technology

Title: Lazy modules

Abstract:

The ML module system is well-known for
its support for modular programming. Motivated by practical
experiences with lazy initialization of modules and the desire to
extend ML modules with recursion, we investigate hybrid evaluation
strategies between call-by-value and call-by-need for ML-style modules
supporting recursion. More precisely we propose and examine five
evaluation strategies: a call-by-value strategy and four call-by-need
strategies with different degrees of laziness.  We formalize the
strategies by translating a source syntax for modules into target
languages, which are very much inspired by Felleisen and Hieb's
call-by-value lambda calculus with state and Ariola and Felleisen's
call-by-need cyclic lambda calculus.  Different strategies are
expressed by tweaking the translation as well as the operational
semantics of the target languages. We look at the strategies through a
series of examples and state inclusion between the strategies.

TSSS 2009-4

Date: 15:00-, Aug 18, 2009

Place: Room SB-1014

Speaker: Naoki Kobayashi, Tohoku University

The datails can be found in the Japanese page.

TSSS 2009-3

Date: 11:00-12:00, Aug 7, 2009

Place: Room SB-1001

Speaker: Franz Winkler, RISC, Johannes Kepler University, Linz, Austria

Title: From Gauss to Groebner and Beyond

Abstract:
Many algorithmic methods in mathematics can be seen
as constructing canonical systems for deciding membership problems.
Important examples are Gauss' elimination method for linear systems,
Euclid's algorithm for computing greatest common divisors,
Buchberger's algorithm for constructing Gr\"obner bases, or
the Knuth-Bendix procedure for equational theories.
We explain the basic concept of canonical systems and investigate
the close connections between these algorithms.

TSSS 2009-2

Date: 10:30-11:30, Jun 19, 2009

Place: Room SB 911-1

Speaker: Prof. Dr.  Helmut Schwichtenberg, Ludwig-Maximilians-Universität, München

Title: Program extraction in constructive analysis

Abstract:
We sketch a development of constructive analysis in Bishop's style,
with special emphasis on low type-level witnesses (using
separability of the reals).  The goal is to set up things in such a
way that realistically executable programs can be extracted from
proofs.  This is carried out for (i) the Intermediate Value Theorem
and (ii) the existence of a continuous inverse to a monotonically
increasing continuous function.  Using the Minlog proof assistant,
the proofs leading to the Intermediate Value Theorem are formalized
and realizing terms extracted.  It turns out that evaluating these
terms is a reasonably fast algorithm to compute, say, approximations
of the square root of 2.

TSSS 2009-1

Date: 3:30 - 15:00, May 1, 2009

Place: SB-1001

Speaker: Dr. Simon Kramer, University of Tsukuba

Title: A General Definition of Malware (joint work with Julian C. Bradfield, U Edinburgh)

Abstract:
We propose a general, formal definition of malware in the language of modal logic. Our definition is
general thanks to its abstract formulation, which, being abstract, is independent of --- but nonetheless
generally applicable to --- the manifold concrete manifestations of malware. From our formulation of
malware, we derive equally general and formal definitions of benware (not malware), anti-malware
(``antibodies'' against malware), and medware (``medicine'' for affected software). We obtain
theoretical tools and practical techniques for the detection, comparison, and classification of malware
and its derivatives. Our general defining principle is causation of (in)correctness.