Search Results

Documents authored by Berger, Ulrich

Document
DOI: 10.4230/LIPIcs.TYPES.2018.1
Martin Hofmann’s Case for Non-Strictly Positive Data Types

Authors: Ulrich Berger, Ralph Matthes, and Anton Setzer

Published in: LIPIcs, Volume 130, 24th International Conference on Types for Proofs and Programs (TYPES 2018)

Abstract
We describe the breadth-first traversal algorithm by Martin Hofmann that uses a non-strictly positive data type and carry out a simple verification in an extensional setting. Termination is shown by implementing the algorithm in the strongly normalising extension of system F by Mendler-style recursion. We then analyze the same algorithm by alternative verifications first in an intensional setting using a non-strictly positive inductive definition (not just a non-strictly positive data type), and subsequently by two different algebraic reductions. The verification approaches are compared in terms of notions of simulation and should elucidate the somewhat mysterious algorithm and thus make a case for other uses of non-strictly positive data types. Except for the termination proof, which cannot be formalised in Coq, all proofs were formalised in Coq and some of the algorithms were implemented in Agda and Haskell.
Cite as

Ulrich Berger, Ralph Matthes, and Anton Setzer. Martin Hofmann’s Case for Non-Strictly Positive Data Types. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 1:1-1:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{berger_et_al:LIPIcs.TYPES.2018.1,
  author =	{Berger, Ulrich and Matthes, Ralph and Setzer, Anton},
  title =	{{Martin Hofmann’s Case for Non-Strictly Positive Data Types}},
  booktitle =	{24th International Conference on Types for Proofs and Programs (TYPES 2018)},
  pages =	{1:1--1:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-106-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{130},
  editor =	{Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.1},
  URN =		{urn:nbn:de:0030-drops-114052},
  doi =		{10.4230/LIPIcs.TYPES.2018.1},
  annote =	{Keywords: non strictly-positive data types, breadth-first traversal, program verification, Mendler-style recursion, System F, theorem proving, Coq, Agda, Haskell}
}
Document
DOI: 10.4230/LIPIcs.CSL.2016.26
Extracting Non-Deterministic Concurrent Programs

Authors: Ulrich Berger

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

Abstract
We introduce an extension of intuitionistic fixed point logic by a modal operator facilitating the extraction of non-deterministic concurrent programs from proofs. We apply this extension to program extraction in computable analysis, more precisely, to computing with Tsuiki's infinite Gray code for real numbers.
Cite as

Ulrich Berger. Extracting Non-Deterministic Concurrent Programs. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 26:1-26:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{berger:LIPIcs.CSL.2016.26,
  author =	{Berger, Ulrich},
  title =	{{Extracting Non-Deterministic Concurrent Programs}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{26:1--26:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.26},
  URN =		{urn:nbn:de:0030-drops-65669},
  doi =		{10.4230/LIPIcs.CSL.2016.26},
  annote =	{Keywords: Proof theory, realizability, program extraction, non-determinism, concurrency, computable analysis}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2013.84
Extracting Imperative Programs from Proofs: In-place Quicksort

Authors: Ulrich Berger, Monika Seisenberger, and Gregory J. M. Woods

Published in: LIPIcs, Volume 26, 19th International Conference on Types for Proofs and Programs (TYPES 2013)

Abstract
The process of program extraction is primarily associated with functional programs with less focus on imperative program extraction. In this paper we consider a standard problem for imperative programming: In-place Quicksort. We formalize a proof that every array of natural numbers can be sorted and apply a realizability interpretation to extract a program from the proof. Using monads we are able to exhibit the inherent imperative nature of the extracted program. We see this as a first step towards an automated extraction of imperative programs. The case study is carried out in the interactive proof assistant Minlog.
Cite as

Ulrich Berger, Monika Seisenberger, and Gregory J. M. Woods. Extracting Imperative Programs from Proofs: In-place Quicksort. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 84-106, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{berger_et_al:LIPIcs.TYPES.2013.84,
  author =	{Berger, Ulrich and Seisenberger, Monika and Woods, Gregory J. M.},
  title =	{{Extracting Imperative Programs from Proofs: In-place Quicksort}},
  booktitle =	{19th International Conference on Types for Proofs and Programs (TYPES 2013)},
  pages =	{84--106},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-72-9},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{26},
  editor =	{Matthes, Ralph and Schubert, Aleksy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.84},
  URN =		{urn:nbn:de:0030-drops-46274},
  doi =		{10.4230/LIPIcs.TYPES.2013.84},
  annote =	{Keywords: Program Extraction, Verification, Realizability, Imperative Programs, In-Place Quicksort,Computational Monads, Minlog}
}
Document
DOI: 10.4230/DagRep.1.10.14
Computing with Infinite Data: Topological and Logical Foundations (Dagstuhl Seminar 11411)

Authors: Ulrich Berger, Vasco Brattka, Victor Selivanov, Dieter Spreen, and Hideki Tsuiki

Published in: Dagstuhl Reports, Volume 1, Issue 10 (2012)

Abstract
There is a large gap between mathematical structures and the structures computer implementations are based on. To stimulate research to overcome this---especially for infinitary structures---highly non-trivial problem the Dagstuhl Seminar 11411 ``Computing with Infinite Data: Topological and Logical Foundations'' was held. This report collects the ideas that were presented and discussed during the course of the seminar.
Cite as

Ulrich Berger, Vasco Brattka, Victor Selivanov, Dieter Spreen, and Hideki Tsuiki. Computing with Infinite Data: Topological and Logical Foundations (Dagstuhl Seminar 11411). In Dagstuhl Reports, Volume 1, Issue 10, pp. 14-36, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@Article{berger_et_al:DagRep.1.10.14,
  author =	{Berger, Ulrich and Brattka, Vasco and Selivanov, Victor and Spreen, Dieter and Tsuiki, Hideki},
  title =	{{Computing with Infinite Data: Topological and Logical Foundations (Dagstuhl Seminar 11411)}},
  pages =	{14--36},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2012},
  volume =	{1},
  number =	{10},
  editor =	{Berger, Ulrich and Brattka, Vasco and Selivanov, Victor and Spreen, Dieter and Tsuiki, Hideki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.1.10.14},
  URN =		{urn:nbn:de:0030-drops-33721},
  doi =		{10.4230/DagRep.1.10.14},
  annote =	{Keywords: Exact real number computation, Stream computation, Infinite computations, Computability in analysis, Hierarchies, Reducibility, Topological complexity}
}
Document
DOI: 10.4230/OASIcs.CCA.2009.2258
Realisability and Adequacy for (Co)induction

Authors: Ulrich Berger

Published in: OASIcs, Volume 11, 6th International Conference on Computability and Complexity in Analysis (CCA'09) (2009)

Abstract
We prove the correctness of a formalised realisability interpretation of extensions of first-order theories by inductive and coinductive definitions in an untyped $\lambda$-calculus with fixed-points. We illustrate the use of this interpretation for program extraction by some simple examples in the area of exact real number computation and hint at further non-trivial applications in computable analysis.
Cite as

Ulrich Berger. Realisability and Adequacy for (Co)induction. In 6th International Conference on Computability and Complexity in Analysis (CCA'09). Open Access Series in Informatics (OASIcs), Volume 11, pp. 49-60, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{berger:OASIcs.CCA.2009.2258,
  author =	{Berger, Ulrich},
  title =	{{Realisability and Adequacy for (Co)induction}},
  booktitle =	{6th International Conference on Computability and Complexity in Analysis (CCA'09)},
  pages =	{49--60},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-12-5},
  ISSN =	{2190-6807},
  year =	{2009},
  volume =	{11},
  editor =	{Bauer, Andrej and Hertling, Peter and Ko, Ker-I},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.CCA.2009.2258},
  URN =		{urn:nbn:de:0030-drops-22581},
  doi =		{10.4230/OASIcs.CCA.2009.2258},
  annote =	{Keywords: Constructive Analysis, realisability, program extraction, semantics}
}
Document
DOI: 10.4230/DagSemProc.04351.11
Continuous Semantics for Termination Proofs

Authors: Ulrich Berger

Published in: Dagstuhl Seminar Proceedings, Volume 4351, Spatial Representation: Discrete vs. Continuous Computational Models (2005)

Abstract
We prove a general strong normalization theorem for higher type rewrite systems based on Tait's strong computability predicates and a strictly continuous domain-theoretic semantics. The theorem applies to extensions of Goedel's system $T$, but also to various forms of bar recursion for which termination was hitherto unknown.
Cite as

Ulrich Berger. Continuous Semantics for Termination Proofs. In Spatial Representation: Discrete vs. Continuous Computational Models. Dagstuhl Seminar Proceedings, Volume 4351, pp. 1-19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2005)

Copy BibTex To Clipboard

@InProceedings{berger:DagSemProc.04351.11,
  author =	{Berger, Ulrich},
  title =	{{Continuous Semantics for Termination Proofs}},
  booktitle =	{Spatial Representation: Discrete vs. Continuous Computational Models},
  pages =	{1--19},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2005},
  volume =	{4351},
  editor =	{Ralph Kopperman and Michael B. Smyth and Dieter Spreen and Julian Webster},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.04351.11},
  URN =		{urn:nbn:de:0030-drops-1300},
  doi =		{10.4230/DagSemProc.04351.11},
  annote =	{Keywords: Higher-order term rewriting , termination , domain theory}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact