DROPS

Document

Well Quasi-Orders in Computer Science (Dagstuhl Seminar 16031)

Authors: Jean Goubault-Larrecq, Monika Seisenberger, Victor Selivanov, and Andreas Weiermann

Published in: Dagstuhl Reports, Volume 6, Issue 1 (2016)

Abstract

This report documents the program and the outcomes of Dagstuhl Seminar 16031 "Well Quasi-Orders in Computer Science", the first seminar devoted to the multiple and deep interactions between the theory of Well quasi-orders (known as the Wqo-Theory) and several fields of Computer Science (Verification and Termination of Infinite-State Systems, Automata and Formal Languages, Term Rewriting and Proof Theory, topological complexity of computational problems on continuous functions). Wqo-Theory is a highly developed part of Combinatorics with ever-growing number of applications in Mathematics and Computer Science, and Well quasi-orders are going to become an important unifying concept of Theoretical Computer Science. In this seminar, we brought together several communities from Computer Science and Mathematics in order to facilitate the knowledge transfer between Mathematicians and Computer Scientists as well as between established and younger researchers and thus to push forward the interaction between Wqo-Theory and Computer Science.

Cite as

Jean Goubault-Larrecq, Monika Seisenberger, Victor Selivanov, and Andreas Weiermann. Well Quasi-Orders in Computer Science (Dagstuhl Seminar 16031). In Dagstuhl Reports, Volume 6, Issue 1, pp. 69-98, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@Article{goubaultlarrecq_et_al:DagRep.6.1.69,
  author =	{Goubault-Larrecq, Jean and Seisenberger, Monika and Selivanov, Victor and Weiermann, Andreas},
  title =	{{Well Quasi-Orders in Computer Science (Dagstuhl Seminar 16031)}},
  pages =	{69--98},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2016},
  volume =	{6},
  number =	{1},
  editor =	{Goubault-Larrecq, Jean and Seisenberger, Monika and Selivanov, Victor and Weiermann, Andreas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.6.1.69},
  URN =		{urn:nbn:de:0030-drops-58158},
  doi =		{10.4230/DagRep.6.1.69},
  annote =	{Keywords: Better quasi-order, Well quasi-order, Hierarchy, Infinite State Machines, Logic, Noetherian space, Reducibility, Termination, Topological Complexity,}
}

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}
}

Search Results

Documents authored by Seisenberger, Monika

Well Quasi-Orders in Computer Science (Dagstuhl Seminar 16031)

Abstract

Cite as

Extracting Imperative Programs from Proofs: In-place Quicksort

Abstract

Cite as

Thanks for your feedback!

Could not send message