Martin Berger

Completeness and Logical Full Abstraction in Modal Logics for Typed Mobile Processes (2009)

Abstract. We propose an extension of Hennessy-Milner logic for the π-calculus which gives sound and complete characterisation of representative behavioural preorder and equivalence over typed...

Fitting 3D Models To 2D Imagery: A Physics Based Approach (2009)

Abstract. We study an extension of Hennessy-Milner logic for the π-calculus which gives a sound and complete characterisation of representative behavioural preorders and equivalences over typed...

Martin Berger, Stefan Scherer

This paper presents a physics based approach to fitting object models to images. The process is modelled as a movement of a rigid body in a viscous environment on a flat surface. The driving forces...

Strong Normalisation in the p-Calculus \Lambda (2009)

Nobuko Yoshida, Martin Berger, Kohei Honda

Acta Zoologica Sinica S22-2 Metabolic aspects of torpor in hummingbirds (2009)

Claus Bech, John F. Steffensen, Martin Berger, Augusto S. Abe

Abstract Tropical species of hummingbirds generally use nightly torpor during which they defend body temperatures (T) of b between 12 and 20°C. We review metabolic aspects in several Brazilian...

Program Logics for Sequential Higher-Order Control ⋆ (2008)

Under consideration for publication in J. Functional Programming 1 Short Note: Verification of In-Place List-Reversal with Effect Sets (2008)

Abstract. We introduce a Hoare logic for higher-order functional languages with control operators such as callcc. The key idea is to build the assertion language and proof rules on the basis of types...

Timed, Distributed, Probabilistic, Typed Processes (2008)

This short note presents a modular correctness proof of a simple in-place list reversal algorithm that is a stable of the relevant literature, cf. (Reynolds, 2002). To keep this note short, we assume...

Abstract A Logical Analysis of Aliasing in Imperative Higher-Order Functions (2008)

Abstract. This paper studies types and probabilistic bisimulations for a timed π-calculus as an effective tool for a compositional analysis of probabilistic distributed behaviour. The types clarify...

Martin Berger, Kohei Honda, Queen Mary, Nobuko Yoshida

We present a compositional program logic for call-by-value imperative higher-order functions with general forms of aliasing, which can arise from the use of reference names as function parameters,...

Logical Reasoning for Higher-Order Functions with Local State (2008)

Yoshida, Nobuko, Honda, Kohei, Berger, Martin

We introduce an extension of Hoare logic for call-by-value higher-order functions with ML-like local reference generation. Local references may be generated dynamically and exported outside their...

Under consideration for publication in J. Functional Programming 1 A Logical Analysis of Aliasing in Imperative Higher-Order Functions (2008)

Logics for Imperative Higher-Order Functions with Aliasing and Local State: Thee Completeness Results (2008)

We present a compositional program logic for call-by-value imperative higher-order functions with general forms of aliasing, which can arise from the use of reference names as function parameters,...

Abstract A Logical Analysis of Aliasing in Imperative Higher-Order Functions (2008)

Abstract. We establish three completeness properties (descriptive, relative and observational completeness) for the program logic for aliasing and higher-order functions, first studied in [1]. We...

Martin Berger, Kohei Honda, Queen Mary, Nobuko Yoshida

We present a compositional program logic for call-by-value imperative higher-order functions with general forms of aliasing, which can arise from the use of reference names as function parameters,...

higher-order functions (2008)

Sequentiality and the ss-Calculus \Lambda (2008)

We present a compositional programme logic for call-by-value imperative higher-order functions with general forms of aliasing, which can arise from the use of reference names as function parameters,...

Under consideration for publication in J. Functional Programming 1 A Logical Analysis of Aliasing in Imperative Higher-Order Functions (2008)

y

We present a compositional program logic for call-by-value imperative higher-order functions with general forms of aliasing, which can arise from the use of reference names as function parameters,...

y, Kohei Honda (2008)

Program Logic and Program Analysis (2008)

z

Sequentiality and the Pi Calculus (2007)

One of the central merits of compositional program logics [18] as a foundation of software engineering is their potential ability to describe a large class of properties of programs relative to a...

Abstract. We present a simple type discipline for the -calculus which precisely captures the notion of sequential functional computation as a specic class of name passing interactive behaviour. The...

The Church-Turing Thesis and Timed Computations (Draft) (2007)

Abstract. We present a simple type discipline for the -calculus which precisely captures the notion of sequential functional computation as a specic class of name passing interactive behaviour. The...

Consider the following program. every 31 seconds print "looking at my Gucci, it's about that time!" Our contentions are simple.

Abstract. We present a simple type discipline for the -calculus which precisely captures the notion of sequential functional computation as a specic class of name passing interactive behaviour. The...

, Kohei Honda (2007)

Abstract.. We present a type discipline for the -calculus which precisely captures the notion of sequential functional computation as a specic class of name passing interactive behaviour. The typed...

Abstract. We present a type discipline for the -calculus which precisely captures the notion of sequential functional computation as a speci c class of name passing interactive behaviour. The typed...

We introduce a typed p-calculus where strong normalisation is ensured by typability. Strong normalisation is a useful property in many computational contexts, including distributed systems. In spite...

Sequentiality and the r-calculus (2007)

Abstract. We introduce a second-order polymorphic -calculus based on duality principles. The calculus and its behavioural theories cleanly capture some of the core elements of signicant technical...

Abstract. We introduce a second-order polymorphic r-calculus based on duality principles. The calculus and its behavioural theories cleanly capture some of the core elements of significant technical...

and Kohei Honda (2007)

We introduce a typed p-calculus where strong normalisation is ensured by typability. Strong normalisation is a useful property in many computational contexts, including distributed systems. In spite...

and Kohei Honda (2007)

We introduce a typed p-calculus where strong normalisation is ensured by typability. Strong normalisation is a useful property in many computational contexts, including distributed systems. In spite...

We introduce a typed p-calculus where strong normalisation is ensured by typability. Strong normalisation is a useful property in many computational contexts, including distributed systems. In spite...

Motion measurements in (2007)

Abstract. We introduce a theory of weak bisimilarity for the -calculus with linear type structure [35] in which we abstract away not only -actions but also non- actions which do not aect well-typed...

Martin Berger, Guido Gerig

1This report has been accepted in shorter form to MICCAI '98. Measuring motion in medical imagery becomes more and more important, in particular for object tracking, image registration, and...

Abstract. Exploiting linear type structure, we introduce a new theory of weak bisimilarity for the -calculus in which we abstract away not only -actions but also non- actions which do not aect...

We introduce a typed p-calculus where strong normalisation is ensured by typability. Strong normalisation is a useful property in many computational contexts, including distributed systems. In spite...

We introduce a typed p-calculus where strong normalisation is ensured by typability. Strong normalisation is a useful property in many computational contexts, including distributed systems. In spite...

Local state in hoare logic for imperative higher-order functions (2007)

We examine extensions to the -calculus for representing basic elements of distributed systems. In spite of its expressiveness for encoding various programming constructs, some of the phenomena...

Local state in hoare logic for imperative higher-order functions (2007)

Abstract. We introduce an extension of Hoare logic for imperative higher-order functions with local state. Local state may be generated dynamically and exported outside its scope, may store...

Logical reasoning for higher-order functions with local state (2006)

Abstract. We introduce an extension of Hoare logic for imperative higher-order functions with local state. Local state may be generated dynamically and exported outside its scope, may store...

Nobuko Yoshida, Kohei Honda, Martin Berger, Queen Mary

Abstract. We introduce an extension of Hoare logic for call-by-value higherorder functions with ML-like local reference generation. Local references may be generated dynamically and exported outside...

Logical reasoning for higher-order functions with local state (2006)

Logical reasoning for higher-order functions with local state (2006)

Abstract. We introduce an extension of Hoare logic for call-by-value higher-order functions with ML-like local reference generation. Local references may be generated dynamically and exported outside...

Nobuko Yoshida, Kohei Honda, Martin Berger, Queen Mary

Abstract. We introduce an extension of Hoare logic for call-by-value higherorder functions with ML-like local reference generation. Local references may be generated dynamically and exported outside...

Logical reasoning for higher-order functions with local state (2006)

Descriptive and relative completeness for logics for higher-order functions (2006)

Abstract. We introduce an extension of Hoare logic for call-by-value higherorder functions with ML-like local reference generation. Local references may be generated dynamically and exported outside...

Kohei Honda, Martin Berger, Nobuko Yoshida

Abstract. This paper establishes a strong completeness property of compositional program logics for pure and imperative higher-order functions introduced in [2, 15–18]. This property, called...

Logical reasoning for higher-order functions with local state (2006)

Deformable area-based template matching with application to low contrast imagery (2005)

Abstract. We introduce an extension of Hoare logic for call-by-value higher-order functions with ML-like local reference generation. Local references may be generated dynamically and exported outside...

Berger, Martin, Gerig, G, Meier, U R, Van Gool, L

An observationally complete program logic for imperative higher-order functions (2005)

An observationally complete program logic for imperative higher-order functions (2005)

Abstract. We propose a simple compositional program logic for an imperative extension of call-by-value PCF, built on Hoare logic and our preceding work on program logics for pure higher-order...

An Observationally Complete Program Logic for Imperative Higher-Order Functions (2005)

We propose a simple compositional program logic for an imperative extension of call-by-value PCF, built on Hoare logic and our preceding work on program logics for pure higher-order functions. A...

An Observationally Complete Program Logic for Imperative Higher-Order Functions (2005)

We propose a simple compositional program logic for an imperative extension of call-by-value PCF, built on Hoare logic and our preceding work on program logics for pure higher-order functions. A...

A Logical Analysis of Aliasing in Imperative Higher-Order Functions (2005)

We propose a simple compositional program logic for an imperative extension of call-by-value PCF, built on Hoare logic and our preceding work on program logics for pure higher-order functions. A...

A logical analysis of aliasing in imperative higher-order functions (2005)

We present a compositional program logic for call-by-value imperative higherorder functions with general forms of aliasing, which can arise from the use of reference names as function parameters,...

An observationally complete program logic for imperative higher-order functions (2005)

Abstract. We present a compositional program logic for call-by-value imperative higherorder functions with general forms of aliasing, which can arise from the use of reference names as function...

An observationally complete program logic for imperative higher-order functions (2005)

We propose a simple compositional program logic for an imperative extension of call-by-value PCF, built on Hoare logic and our preceding work on program logics for pure higher-order functions. A...

Personalrecht für die Praxis 2004: Arbeitsrecht, Lohnsteuer und Sozialversicherung. (2004)

Abstract. We propose a simple compositional program logic for an imperative extension of call-by-value PCF, built on Hoare logic and our preceding work on program logics for pure higher-order...

Bartone, Roberto, Berger, Martin, Brösske, Christof

Dieses Rechtshandbuch schafft eine systematische Vernetzung der Bereiche Arbeits-, Sozialversicherungs- und Lohnsteuerrecht und zeigt damit alle Aspekte auf, die im Zusammenhang mit einer konkreten...

Basic theory of reduction congruence for two timed asynchronous π-calculi (2004)

Basic theory of reduction congruence for two timed asynchronous π-calculi (2004)

Abstract. We study reduction congruence, a popular notion of process equality, for the asynchronous -calculus with timers, and derive several alternative characterisations, one of them being a...

The Church-Turing Thesis and Timed Computations (Draft) Consider the following program. (2004)

Abstract. We study reduction congruence, a popular notion of process equality, for the asynchronous π-calculus with timers, and derive several alternative characterisations, one of them being a...

Genericity and the π-Calculus (2003)

every 31 seconds print "looking at my Gucci, it’s about that time!" Our contentions are simple.

Towards Abstractions for Distributed Systems (2002)

Types in processes delineate specific classes of interactive behaviour in a compositional way. Key elements of process theory, in particular behavioural equivalences, are deeply affected by types,...

Linearity and bisimulation (2002)

N ~ ao posso querer ser nada. A parte isso, tenho em mim todos os sonhos do mundo." iii iv For historical, sociological and technical reasons, -calculi have been the dominant theoretical...

Towards Abstractions for Distributed Systems (2002)

Abstract. Exploiting linear type structure, we introduce a new theory of weak bisimilarity for the π-calculus in which we abstract away not only τ-actions but also non-τ actions which do not...

Sequentiality and the π-calculus (2001)

“Não sou nada.

Sequentiality and the -calculus (2001)

We introduce a second-order polymorphic π-calculus based on duality principles. The calculus and its behavioural theories cleanly capture some of the core elements of significant technical...

Sequentiality and the -calculus (2001)

Abstract. We introduce a second-order polymorphic -calculus based on duality principles. The calculus and its behavioural theories cleanly capture some of the core elements of signicant technical...

Tiefe Sedierung mit Propofol zur zahnärztlichen Gebisssanierung bei behandlungsunwilligen Kindern im Vorschulalter / (2000)

Abstract. Types in processes delineate specic classes of interactive behaviour in a compositional way. Key elements of process theory, in particular behavioural equivalences, are deeply aected by...

Untersuchungen an wartungsfreien trockenlaufenden Verbundgleitlagern / (2000)

Thesis (doctoral)--Ludwig-Maximilians-Universitat zu Munchen, 2000.

The Two-Phase Commitment Protocol in an Extended π-Calculus (2000)

Zugl.: Magdeburg, Universiẗat, Diss., 2000.

Martin Berger, Kohei Honda

We examine extensions to the -calculus for representing basic elements of distributed systems. In spite of its expressiveness for encoding various programming constructs, some of the phenomena...

Towards Abstractions for Distributed Systems (2000)

Deformable area-based template matching with application to low contrast imagery (1999)

For historical, sociological and technical reasons, -calculi have been the dominant theoretical paradigm in the study of functional computation. Similarly, but to a lesser degree, -calculi dominate...

Berger, Martin

Deformable area based template matching with application to low contrast imagery /--Martin Berger. (1999)

Deformable area-based template matching with application to low contrast imagery / (1999)

Thesis (doctoral) - Eidgenössische Technische Hochschschule, Zürich, 1999.

Motion measurements in low-contrast X-ray imagery (1998)

Diss. Nr. 13144 techn. Wiss. ETH Zürich.

Martin Berger, Guido Gerig

Measuring motion in medical imagery becomes more and more important, in particular for object tracking, image registration, and local displacement measurements. Often, the requirements on the...

The Framework of Least Squares Template Matching (1998)

Deformable Area-based Template Matching with Application to Low Contrast Imagery (1998)

The accurate registration of image series and exact matching of image parts is essential to numerous problems in computer vision. The framework presented in this paper is a generic matching algorithm...

Martin Berger, Guido Gerig

This paper reviews the mathematical formalism of the least squares template matching (LSM) and presents a framework for automatic quality control of the resulting match. LSM is an iterative and...

Geld oder private Lebensqualität? : Was studierende von ihrem späteren Job erwarten (1997)

Krebs, Dagmar, Berger, Martin

Deformable Multi Template Matching with Application to Portal Images (1997)

Martin Berger, Gaudenz Danuser

This report has been submitted to CVPR'97. The exact positioning of patients during radiotherapy is essential for high precision treatment. The registration of portal image sequences...

Deformable Multi Template Matching with Application to Portal Images (1997)

Martin Berger, Gaudenz Danuser

The exact positioning of patients during radiotherapy is essential for high precision treatment. The registration of portal image sequences can help to control the patient position. The particular...

Detection and characterization of unsharp blobs by curve evolution (1995)

G. Gerig, Guido Gerig, Guido Gerig, Georg Israel, Georg Israel, Georg Israel, ...

Abstract This paper presents a novel method for the multi-scale segmentation and shape characterization of unsharp, blobby structures in gray-valued image data. The iso-level curves of unsharp blobs...

Untersuchungen über die Reaktionsgeschwindigkeit von Warmblütern bei kurzen optischen und akustischen Reizen. (1961)