9 Search Results for "Hofmann, Peter"

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-dev.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/DagSemProc.06141.17
Reliability-Aware Power Management Of Multi-Core Systems (MPSoCs)

Authors: Klaus Waldschmidt, Jan Haase, Andreas Hofmann, Markus Damm, and Dennis Hauser

Published in: Dagstuhl Seminar Proceedings, Volume 6141, Dynamically Reconfigurable Architectures (2006)

Abstract
Long-term reliability of processors in embedded systems is experiencing growing attention since decreasing feature sizes and increasing power consumption have a negative influence on the lifespan. Among other measures, the reliability can be influenced significantly by Dynamic Power Management (DPM), since it affects the processor's temperature. Compared to single-core systems reconfigurable multi-core SoCs offer much more possibilities to optimize power and reliability. The impact of different DPM-strategies on the lifespan of multi-core processors is the focus of this presentation. It is shown that the long-term reliability of a multi-core system can be influenced deliberately with different DPM strategies and that temperature cycling greatly influences the estimated lifespan. In this presentation, a new reliability-aware dynamic power management (RADPM) policy is explained.
Cite as

Klaus Waldschmidt, Jan Haase, Andreas Hofmann, Markus Damm, and Dennis Hauser. Reliability-Aware Power Management Of Multi-Core Systems (MPSoCs). In Dynamically Reconfigurable Architectures. Dagstuhl Seminar Proceedings, Volume 6141, pp. 1-7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{waldschmidt_et_al:DagSemProc.06141.17,
  author =	{Waldschmidt, Klaus and Haase, Jan and Hofmann, Andreas and Damm, Markus and Hauser, Dennis},
  title =	{{Reliability-Aware Power Management Of Multi-Core Systems (MPSoCs)}},
  booktitle =	{Dynamically Reconfigurable Architectures},
  pages =	{1--7},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6141},
  editor =	{Peter M. Athanas and J\"{u}rgen Becker and Gordon Brebner and J\"{u}rgen Teich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.06141.17},
  URN =		{urn:nbn:de:0030-drops-7458},
  doi =		{10.4230/DagSemProc.06141.17},
  annote =	{Keywords: Organic computing, Adaptivity, Power Management, Power Consumption, Reliability, SDVM}
}
Document
DOI: 10.4230/DagSemProc.06031.1
06031 Abstracts Collection – Organic Computing – Controlled Emergence

Authors: Kirstie Bellman, Peter Hofmann, Christian Müller-Schloer, Hartmut Schmeck, and Rolf P. Würtz

Published in: Dagstuhl Seminar Proceedings, Volume 6031, Organic Computing - Controlled Emergence (2006)

Abstract
Organic Computing has emerged recently as a challenging vision for future information processing systems, based on the insight that we will soon be surrounded by large collections of autonomous systems equipped with sensors and actuators to be aware of their environment, to communicate freely, and to organize themselves in order to perform the actions and services required. Organic Computing Systems will adapt dynamically to the current conditions of its environment, they will be self-organizing, self-configuring, self-healing, self-protecting, self-explaining, and context-aware. From 15.01.06 to 20.01.06, the Dagstuhl Seminar 06031 ``Organic Computing – Controlled Emergence'' was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. The seminar was characterized by the very constructive search for common ground between engineering and natural sciences, between informatics on the one hand and biology, neuroscience, and chemistry on the other. The common denominator was the objective to build practically usable self-organizing and emergent systems or their components. An indicator for the practical orientation of the seminar was the large number of OC application systems, envisioned or already under implementation, such as the Internet, robotics, wireless sensor networks, traffic control, computer vision, organic systems on chip, an adaptive and self-organizing room with intelligent sensors or reconfigurable guiding systems for smart office buildings. The application orientation was also apparent by the large number of methods and tools presented during the seminar, which might be used as building blocks for OC systems, such as an evolutionary design methodology, OC architectures, especially several implementations of observer/controller structures, measures and measurement tools for emergence and complexity, assertion-based methods to control self-organization, wrappings, a software methodology to build reflective systems, and components for OC middleware. Organic Computing is clearly oriented towards applications but is augmented at the same time by more theoretical bio-inspired and nature-inspired work, such as chemical computing, theory of complex systems and non-linear dynamics, control mechanisms in insect swarms, homeostatic mechanisms in the brain, a quantitative approach to robustness, abstraction and instantiation as a central metaphor for understanding complex systems. Compared to its beginnings, Organic Computing is coming of age. The OC vision is increasingly padded with meaningful applications and usable tools, but the path towards full OC systems is still complex. There is progress in a more scientific understanding of emergent processes. In the future, we must understand more clearly how to open the configuration space of technical systems for on-line modification. Finally, we must make sure that the human user remains in full control while allowing the systems to optimize.
Cite as

Kirstie Bellman, Peter Hofmann, Christian Müller-Schloer, Hartmut Schmeck, and Rolf P. Würtz. 06031 Abstracts Collection – Organic Computing – Controlled Emergence. In Organic Computing - Controlled Emergence. Dagstuhl Seminar Proceedings, Volume 6031, pp. 1-19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{bellman_et_al:DagSemProc.06031.1,
  author =	{Bellman, Kirstie and Hofmann, Peter and M\"{u}ller-Schloer, Christian and Schmeck, Hartmut and W\"{u}rtz, Rolf P.},
  title =	{{06031 Abstracts Collection – Organic Computing – Controlled Emergence}},
  booktitle =	{Organic Computing - Controlled Emergence},
  pages =	{1--19},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6031},
  editor =	{Kirstie Bellman and Peter Hofmann and Christian M\"{u}ller-Schloer and Hartmut Schmeck and Rolf W\"{u}rtz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.06031.1},
  URN =		{urn:nbn:de:0030-drops-5777},
  doi =		{10.4230/DagSemProc.06031.1},
  annote =	{Keywords: Emergence, self-organization, self-configuration, self-healing, self-protection, self-explaining, context-awareness}
}
Document
DOI: 10.4230/DagSemProc.06031.2
06031 Executive Summary – Organic Computing – Controlled Emergence

Authors: Kirstie Bellman, Peter Hofmann, Christian Müller-Schloer, Hartmut Schmeck, and Rolf P. Würtz

Published in: Dagstuhl Seminar Proceedings, Volume 6031, Organic Computing - Controlled Emergence (2006)

Abstract
Organic Computing has emerged recently as a challenging vision for future information processing systems, based on the insight that we will soon be surrounded by systems with massive numbers of processing elements, sensors and actuators, many of which will be autonomous. Because of the size of these systems it is infeasible for us to monitor and control them entirely from external observations; instead they will need to help us monitor, control and adapt themselves. To do so, these components will need to be aware of their environment, to communicate freely, and to organize themselves in order to perform the actions and services that are required. The presence of networks of intelligent systems in our environment opens up fascinating application areas but, at the same time, bears the problem of their controllability. Hence, we have to construct these systems which we increasingly depend on as robust, safe, flexible, and trustworthy as possible. In particular, a strong orientation towards human needs as opposed to a pure implementation of the technologically possible seems absolutely central. In order to achieve these goals, our technical systems will have to act more independently, flexibly, and autonomously, i.e., they will have to exhibit lifelike properties. We call those systems ''organic''. Hence, an ''Organic Computing System'' is a technical system which adapts dynamically to the current conditions of its environment. It will be selforganizing, selfconfiguring, selfhealing, selfprotecting, selfexplaining, and context-aware.
Cite as

Kirstie Bellman, Peter Hofmann, Christian Müller-Schloer, Hartmut Schmeck, and Rolf P. Würtz. 06031 Executive Summary – Organic Computing – Controlled Emergence. In Organic Computing - Controlled Emergence. Dagstuhl Seminar Proceedings, Volume 6031, pp. 1-3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{bellman_et_al:DagSemProc.06031.2,
  author =	{Bellman, Kirstie and Hofmann, Peter and M\"{u}ller-Schloer, Christian and Schmeck, Hartmut and W\"{u}rtz, Rolf P.},
  title =	{{06031 Executive Summary – Organic Computing – Controlled Emergence}},
  booktitle =	{Organic Computing - Controlled Emergence},
  pages =	{1--3},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6031},
  editor =	{Kirstie Bellman and Peter Hofmann and Christian M\"{u}ller-Schloer and Hartmut Schmeck and Rolf W\"{u}rtz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.06031.2},
  URN =		{urn:nbn:de:0030-drops-5788},
  doi =		{10.4230/DagSemProc.06031.2},
  annote =	{Keywords: Emergence, self-organization, self-configuration, self-healing, self-protection, self-explaining, context-awareness}
}
Document
DOI: 10.4230/DagSemProc.06031.3
Benefits of Bio-inspired Technologies for Networked Embedded Systems: An Overview

Authors: Falko Dressler

Published in: Dagstuhl Seminar Proceedings, Volume 6031, Organic Computing - Controlled Emergence (2006)

Abstract
The communication between networked embedded systems has become a major research domain in the communication networks area. Wireless sensor networks (WSN) and sensor/actuator networks (SANET) build of huge amounts of interacting nodes build the basis for this research. Issues such as mobility, network size, deployment density, and energy are the key factors for the development of new communication methodologies. Self-organization mechanisms promise to solve scalability problems – unfortunately, by decreasing the determinism and the controllability of the overall system. Self-Organization was first studied in nature and its design principles such as feedback loops and the behavior on local information have been adapted to technical systems. Bio-inspired networking is the keyword in the communications domain. In this paper, selected bio-inspired technologies and their applicability for sensor/actuator networks are discussed. This includes for example the artificial immune system, swarm intelligence, and the intercellular information exchange.
Cite as

Falko Dressler. Benefits of Bio-inspired Technologies for Networked Embedded Systems: An Overview. In Organic Computing - Controlled Emergence. Dagstuhl Seminar Proceedings, Volume 6031, pp. 1-10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{dressler:DagSemProc.06031.3,
  author =	{Dressler, Falko},
  title =	{{Benefits of Bio-inspired Technologies for Networked Embedded Systems: An Overview}},
  booktitle =	{Organic Computing - Controlled Emergence},
  pages =	{1--10},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6031},
  editor =	{Kirstie Bellman and Peter Hofmann and Christian M\"{u}ller-Schloer and Hartmut Schmeck and Rolf W\"{u}rtz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.06031.3},
  URN =		{urn:nbn:de:0030-drops-5761},
  doi =		{10.4230/DagSemProc.06031.3},
  annote =	{Keywords: Bio-inspired networking, self-organization, wireless sensor network, sensor/actuator network}
}
Document
DOI: 10.4230/DagSemProc.06031.4
Ercatons and Organic Programming: Say Good-Bye to Planned Economy

Authors: Falk Langhammer, Oliver Imbusch, and Guido von Walter

Published in: Dagstuhl Seminar Proceedings, Volume 6031, Organic Computing - Controlled Emergence (2006)

Abstract
Organic programming (OP) is our proposed and already emerging programming model which overcomes some of the limitations of current practice in software development in general and of object-oriented programming (OOP) in particular. Ercatons provide an implementation of the model. In some respects, OP is less than a (new) programming language, in others, it is more. An "ercato machine" implements the ideas discussed and has been used to validate the concepts described here. Organic programming is centered around the concept of a true "Thing". A thing in an executing software system is bound to behave the way an autonomous object does in our real world, or like a cell does in an organism. Software objects do not. Therefore, traditional software systems must be planned while with OP, software systems grow. This fact is traced back to be the root why current software development often fails to meet our expectations when it comes to large-scale projects. OP should then be able to provide the means to make software development achieve what other engineering disciplines have achieved a long time ago: that project effort scales sub-linearly with size. With OP we introduce a new term because we hope that the approach we are pursuing is radical enough to justify this.
Cite as

Falk Langhammer, Oliver Imbusch, and Guido von Walter. Ercatons and Organic Programming: Say Good-Bye to Planned Economy. In Organic Computing - Controlled Emergence. Dagstuhl Seminar Proceedings, Volume 6031, pp. 1-11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{langhammer_et_al:DagSemProc.06031.4,
  author =	{Langhammer, Falk and Imbusch, Oliver and von Walter, Guido},
  title =	{{Ercatons and Organic Programming: Say Good-Bye to Planned Economy}},
  booktitle =	{Organic Computing - Controlled Emergence},
  pages =	{1--11},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6031},
  editor =	{Kirstie Bellman and Peter Hofmann and Christian M\"{u}ller-Schloer and Hartmut Schmeck and Rolf W\"{u}rtz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.06031.4},
  URN =		{urn:nbn:de:0030-drops-5744},
  doi =		{10.4230/DagSemProc.06031.4},
  annote =	{Keywords: Organic, software engineering}
}
Document
DOI: 10.4230/DagSemProc.06031.5
Feature-driven Emergence of Model Graphs for Object Recognition and Categorization

Authors: Günter Westphal, Christoph von der Malsburg, and Rolf P. Würtz

Published in: Dagstuhl Seminar Proceedings, Volume 6031, Organic Computing - Controlled Emergence (2006)

Abstract
An important requirement for the expression of cognitive structures is the ability to form mental objects by rapidly binding together constituent parts. In this sense, one may conceive the brain's data structure to have the form of graphs whose nodes are labeled with elementary features. These provide a versatile data format with the additional ability to render the structure of any mental object. Because of the multitude of possible object variations the graphs are required to be dynamic. Upon presentation of an image a so-called model graph should rapidly emerge by binding together memorized subgraphs derived from earlier learning examples driven by the image features. In this model, the richness and flexibility of the mind is made possible by a combinatorical game of immense complexity. Consequently, the emergence of model graphs is a laborious task which, in computer vision, has most often been disregarded in favor of employing model graphs tailored to specific object categories like, for instance, faces in frontal pose. Recognition or categorization of arbitrary objects, however, demands dynamic graphs. In this work we propose a form of graph dynamics, which proceeds in two steps. In the first step component classifiers, which decide whether a feature is present in an image, are learned from training images. For processing arbitrary objects, features are small localized grid graphs, so-called parquet graphs, whose nodes are attributed with Gabor amplitudes. Through combination of these classifiers into a linear discriminant that conforms to Linsker's infomax principle a weighted majority voting scheme is implemented. It allows for preselection of salient learning examples, so-called model candidates, and likewise for preselection of categories the object in the presented image supposably belongs to. Each model candidate is verified in a second step using a variant of elastic graph matching, a standard correspondence-based technique for face and object recognition. To further differentiate between model candidates with similar features it is asserted that the features be in similar spatial arrangement for the model to be selected. Model graphs are constructed dynamically by assembling model features into larger graphs according to their spatial arrangement. From the viewpoint of pattern recognition, the presented technique is a combination of a discriminative (feature-based) and a generative (correspondence-based) classifier while the majority voting scheme implemented in the feature-based part is an extension of existing multiple feature subset methods. We report the results of experiments on standard databases for object recognition and categorization. The method achieved high recognition rates on identity, object category, pose, and illumination type. Unlike many other models the presented technique can also cope with varying background, multiple objects, and partial occlusion.
Cite as

Günter Westphal, Christoph von der Malsburg, and Rolf P. Würtz. Feature-driven Emergence of Model Graphs for Object Recognition and Categorization. In Organic Computing - Controlled Emergence. Dagstuhl Seminar Proceedings, Volume 6031, pp. 1-46, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{westphal_et_al:DagSemProc.06031.5,
  author =	{Westphal, G\"{u}nter and von der Malsburg, Christoph and W\"{u}rtz, Rolf P.},
  title =	{{Feature-driven Emergence of Model Graphs for Object Recognition and Categorization}},
  booktitle =	{Organic Computing - Controlled Emergence},
  pages =	{1--46},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6031},
  editor =	{Kirstie Bellman and Peter Hofmann and Christian M\"{u}ller-Schloer and Hartmut Schmeck and Rolf W\"{u}rtz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.06031.5},
  URN =		{urn:nbn:de:0030-drops-5756},
  doi =		{10.4230/DagSemProc.06031.5},
  annote =	{Keywords: Graph matching, recognition, categorization, computer vision, self-organization, emergence}
}
Document
DOI: 10.4230/DagSemProc.05471.8
Glycosylation Patterns of Proteins Studied by Liquid Chromatography-Mass Spectrometry and Bioinformatic Tools

Authors: Hansjörg Toll, Peter Berger, Andreas Hofmann, Andreas Hildebrandt, Herbert Oberacher, Hans Peter Lenhof, and Christian G. Huber

Published in: Dagstuhl Seminar Proceedings, Volume 5471, Computational Proteomics (2006)

Abstract
Due to their extensive structural heterogeneity, the elucidation of glycosylation patterns in glycoproteins such as the subunits of chorionic gonadotropin (CG), CG-alpha and CG-beta remains one of the most challenging problems in the proteomic analysis of posttranslational modifications. In consequence, glycosylation is usually studied after decomposition of the intact proteins to the proteolytic peptide level. However, by this approach all information about the combination of the different glycopeptides in the intact protein is lost. In this study we have, therefore, attempted to combine the results of glycan identification after tryptic digestion with molecular mass measurements on the intact glycoproteins. Despite the extremely high number of possible combinations of the glycans identified in the tryptic peptides by high-performance liquid chromatography-mass spectrometry (> 1000 for CG-alpha and > 10.000 for CG-beta), the mass spectra of intact CG-alpha and CG-beta revealed only a limited number of glycoforms present in CG preparations from pools of pregnancy urines. Peak annotations for CG-alpha were performed with the help of an algorithm that generates a database containing all possible modifications of the proteins (inclusive possible artificial modifications such as oxidation or truncation) and subsequent searches for combinations fitting the mass difference between the polypeptide backbone and the measured molecular masses. Fourteen different glycoforms of CG-alpha, including methionine-oxidized and N-terminally truncated forms, were readily identified. For CG-beta, however, the relatively high mass accuracy of ± 2 Da was still insufficient to unambiguously assign the possible combinations of posttranslational modifications. Finally, the mass spectrometric fingerprints of the intact molecules were shown to be very useful for the characterization of glycosylation patterns in different CG preparations.
Cite as

Hansjörg Toll, Peter Berger, Andreas Hofmann, Andreas Hildebrandt, Herbert Oberacher, Hans Peter Lenhof, and Christian G. Huber. Glycosylation Patterns of Proteins Studied by Liquid Chromatography-Mass Spectrometry and Bioinformatic Tools. In Computational Proteomics. Dagstuhl Seminar Proceedings, Volume 5471, pp. 1-6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{toll_et_al:DagSemProc.05471.8,
  author =	{Toll, Hansj\"{o}rg and Berger, Peter and Hofmann, Andreas and Hildebrandt, Andreas and Oberacher, Herbert and Lenhof, Hans Peter and Huber, Christian G.},
  title =	{{Glycosylation Patterns of Proteins Studied by Liquid Chromatography-Mass Spectrometry and Bioinformatic Tools}},
  booktitle =	{Computational Proteomics},
  pages =	{1--6},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5471},
  editor =	{Christian G. Huber and Oliver Kohlbacher and Knut Reinert},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.05471.8},
  URN =		{urn:nbn:de:0030-drops-5431},
  doi =		{10.4230/DagSemProc.05471.8},
  annote =	{Keywords: Liquid chromatography, mass spectrometry, glycoproteins, glycosylation, peak annotation}
}
Document
DOI: 10.4230/DagSemProc.04381.2
Interactive Programs and Weakly Final Coalgebras in Dependent Type Theory (Extended Version)

Authors: Anton Setzer and Peter Hancock

Published in: Dagstuhl Seminar Proceedings, Volume 4381, Dependently Typed Programming (2005)

Abstract
We reconsider the representation of interactive programs in dependent type theory that the authors proposed in earlier papers. Whereas in previous versions the type of interactive programs was introduced in an ad hoc way, it is here defined as a weakly final coalgebra for a general form of polynomial functor. The are two versions: in the first the interface with the real world is fixed, while in the second the potential interactions can depend on the history of previous interactions. The second version may be appropriate for working with specifications of interactive programs. We focus on command-response interfaces, and consider both client and server programs, that run on opposite sides such an interface. We give formation/introduction/elimination/equality rules for these coalgebras. These are explored in two dimensions: coiterative versus corecursive, and monadic versus non-monadic. We also comment upon the relationship of the corresponding rules with guarded induction. It turns out that the introduction rules are nothing but a slightly restricted form of guarded induction. However, the form in which we write guarded induction is not recursive equations (which would break normalisation – we show that type checking becomes undecidable), but instead involves an elimination operator in a crucial way.
Cite as

Anton Setzer and Peter Hancock. Interactive Programs and Weakly Final Coalgebras in Dependent Type Theory (Extended Version). In Dependently Typed Programming. Dagstuhl Seminar Proceedings, Volume 4381, pp. 1-30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2005)

Copy BibTex To Clipboard

@InProceedings{setzer_et_al:DagSemProc.04381.2,
  author =	{Setzer, Anton and Hancock, Peter},
  title =	{{Interactive Programs and Weakly Final Coalgebras in Dependent Type Theory (Extended Version)}},
  booktitle =	{Dependently Typed Programming},
  pages =	{1--30},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2005},
  volume =	{4381},
  editor =	{Thorsten Altenkirch and Martin Hofmann and John Hughes},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.04381.2},
  URN =		{urn:nbn:de:0030-drops-1768},
  doi =		{10.4230/DagSemProc.04381.2},
  annote =	{Keywords: Dependently types programming , interactive programs , coalgebras , weakly final coalgebras , coiteration , corecursion , monad}
}
  • Refine by Author
  • 3 Würtz, Rolf P.
  • 2 Bellman, Kirstie
  • 2 Hofmann, Andreas
  • 2 Hofmann, Peter
  • 2 Müller-Schloer, Christian
  • Show More...

  • Refine by Classification
  • 1 Software and its engineering → Abstract data types
  • 1 Software and its engineering → Coroutines
  • 1 Software and its engineering → Recursion
  • 1 Software and its engineering → Software verification
  • 1 Theory of computation → Logic and verification
  • Show More...

  • Refine by Keyword
  • 4 self-organization
  • 2 Emergence
  • 2 context-awareness
  • 2 self-configuration
  • 2 self-explaining
  • Show More...

  • Refine by Type
  • 9 document

  • Refine by Publication Year
  • 7 2006
  • 1 2005
  • 1 2019

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