5 Search Results for "Hildebrandt, Andreas"

Document
DOI: 10.4230/LIPIcs.ITP.2025.30
Nondeterministic Asynchronous Dataflow in Isabelle/HOL

Authors: Rafael Castro Gonçalves Silva, Laouen Fernet, and Dmitriy Traytel

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
We formalize nondeterministic asynchronous dataflow networks in Isabelle/HOL. Dataflow networks are comprised of operators that are capable of communicating with the network, performing silent computations, and making nondeterministic choices. We represent operators using a shallow embedding as codatatypes. Using this representation, we define standard asynchronous dataflow primitives, including sequential and parallel composition and a feedback operator. These primitives adhere to a number of laws from the literature, which we prove by coinduction using weak bisimilarity as our equality. Albeit coinductive and nondeterministic, our model is executable via code extraction to Haskell.
Cite as

Rafael Castro Gonçalves Silva, Laouen Fernet, and Dmitriy Traytel. Nondeterministic Asynchronous Dataflow in Isabelle/HOL. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 30:1-30:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{silva_et_al:LIPIcs.ITP.2025.30,
  author =	{Silva, Rafael Castro Gon\c{c}alves and Fernet, Laouen and Traytel, Dmitriy},
  title =	{{Nondeterministic Asynchronous Dataflow in Isabelle/HOL}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{30:1--30:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.30},
  URN =		{urn:nbn:de:0030-drops-246280},
  doi =		{10.4230/LIPIcs.ITP.2025.30},
  annote =	{Keywords: dataflow, verification, coinduction, Isabelle/HOL}
}
Document
DOI: 10.4230/OASIcs.SpaceCHI.2025.7
Unbound Human-Machine Interfaces for Interaction in Weightless Environments

Authors: Jessica R. Cauchard

Published in: OASIcs, Volume 130, Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025)

Abstract
User interfaces are subject to the rules of physics (e.g., Newton and Archimedes' laws) relevant to the environment they are in. As such, most interfaces and interaction techniques have been designed for Earth surface. However, when interacting with technology in weightless environments, such as in space, both human and machine will be subject to different physical constraints. For instance, underwater or in Space, people can experience spatial disorientation, which will in turn affect how they use a system. This position paper conceptualizes unbound Human-Machine Interfaces (HMIs) as interfaces where either, or both, human and machine are located beyond Earth surface. In particular, it describes how traditional HCI needs to be rethought for interaction in weightless environments and how theoretical models such as joint cognition can support future developments of unbound interfaces.
Cite as

Jessica R. Cauchard. Unbound Human-Machine Interfaces for Interaction in Weightless Environments. In Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025). Open Access Series in Informatics (OASIcs), Volume 130, pp. 7:1-7:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{cauchard:OASIcs.SpaceCHI.2025.7,
  author =	{Cauchard, Jessica R.},
  title =	{{Unbound Human-Machine Interfaces for Interaction in Weightless Environments}},
  booktitle =	{Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025)},
  pages =	{7:1--7:8},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-384-3},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{130},
  editor =	{Bensch, Leonie and Nilsson, Tommy and Nisser, Martin and Pataranutaporn, Pat and Schmidt, Albrecht and Sumini, Valentina},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SpaceCHI.2025.7},
  URN =		{urn:nbn:de:0030-drops-239970},
  doi =		{10.4230/OASIcs.SpaceCHI.2025.7},
  annote =	{Keywords: human-robot interaction, gravity, space, interaction technique}
}
Document
DOI: 10.4230/OASIcs.GCB.2013.56
Efficient Interpretation of Tandem Mass Tags in Top-Down Proteomics

Authors: Anna Katharina Hildebrandt, Ernst Althaus, Hans-Peter Lenhof, Chien-Wen Hung, Andreas Tholey, and Andreas Hildebrandt

Published in: OASIcs, Volume 34, German Conference on Bioinformatics 2013

Abstract
Mass spectrometry is the major analytical tool for the identification and quantification of proteins in biological samples. In so-called top-down proteomics, separation and mass spectrometric analysis is performed at the level of intact proteins, without preparatory digestion steps. It has been shown that the tandem mass tag (TMT) labeling technology, which is often used for quantification based on digested proteins (bottom-up studies), can be applied in top-down proteomics as well. This, however, leads to a complex interpretation problem, where we need to annotate measured peaks with their respective generating protein, the number of charges, and the a priori unknown number of TMT-groups attached to this protein. In this work, we give an algorithm for the efficient enumeration of all valid annotations that fulfill available experimental constraints. Applying the algorithm to real-world data, we show that the annotation problem can indeed be efficiently solved. However, our experiments also demonstrate that reliable annotation in complex mixtures requires at least partial sequence information and high mass accuracy and resolution to go beyond the proof-of-concept stage.
Cite as

Anna Katharina Hildebrandt, Ernst Althaus, Hans-Peter Lenhof, Chien-Wen Hung, Andreas Tholey, and Andreas Hildebrandt. Efficient Interpretation of Tandem Mass Tags in Top-Down Proteomics. In German Conference on Bioinformatics 2013. Open Access Series in Informatics (OASIcs), Volume 34, pp. 56-67, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{hildebrandt_et_al:OASIcs.GCB.2013.56,
  author =	{Hildebrandt, Anna Katharina and Althaus, Ernst and Lenhof, Hans-Peter and Hung, Chien-Wen and Tholey, Andreas and Hildebrandt, Andreas},
  title =	{{Efficient Interpretation of Tandem Mass Tags in Top-Down Proteomics}},
  booktitle =	{German Conference on Bioinformatics 2013},
  pages =	{56--67},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-59-0},
  ISSN =	{2190-6807},
  year =	{2013},
  volume =	{34},
  editor =	{Bei{\ss}barth, Tim and Kollmar, Martin and Leha, Andreas and Morgenstern, Burkhard and Schultz, Anne-Kathrin and Waack, Stephan and Wingender, Edgar},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.GCB.2013.56},
  URN =		{urn:nbn:de:0030-drops-42304},
  doi =		{10.4230/OASIcs.GCB.2013.56},
  annote =	{Keywords: Mass spectrometry, TMT labeling, Top-down Proteomics}
}
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.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.05471.9
High-accuracy peak picking of proteomics data

Authors: Eva Lange, Clemens Gröpl, Oliver Kohlbacher, and Andreas Hildebrandt

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

Abstract
A new peak picking algorithm for the analysis of mass spectrometric (MS) data is presented. It is independent of the underlying machine or ionization method, and is able to resolve highly convoluted and asymmetric signals. The method uses the multiscale nature of spectrometric data by first detecting the mass peaks in the wavelet-transformed signal before a given asymmetric peak function is fitted to the raw data. In an optional third stage, the resulting fit can be further improved using techniques from nonlinear optimization. In contrast to currently established techniques (e.g. SNAP, Apex) our algorithm is able to separate overlapping peaks of multiply charged peptides in ESI-MS data of low resolution. Its improved accuracy with respect to peak positions makes it a valuable preprocessing method for MS-based identification and quantification experiments. The method has been validated on a number of different annotated test cases, where it compares favorably in both runtime and accuracy with currently established techniques. An implementation of the algorithm is freely available in our open source framework OpenMS (www.open-ms.de).
Cite as

Eva Lange, Clemens Gröpl, Oliver Kohlbacher, and Andreas Hildebrandt. High-accuracy peak picking of proteomics data. In Computational Proteomics. Dagstuhl Seminar Proceedings, Volume 5471, pp. 1-9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{lange_et_al:DagSemProc.05471.9,
  author =	{Lange, Eva and Gr\"{o}pl, Clemens and Kohlbacher, Oliver and Hildebrandt, Andreas},
  title =	{{High-accuracy peak picking of proteomics data}},
  booktitle =	{Computational Proteomics},
  pages =	{1--9},
  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.dagstuhl.de/entities/document/10.4230/DagSemProc.05471.9},
  URN =		{urn:nbn:de:0030-drops-5358},
  doi =		{10.4230/DagSemProc.05471.9},
  annote =	{Keywords: Mass spectrometry, peak detection, peak picking}
}
  • Refine by Type
  • 5 Document/PDF
  • 2 Document/HTML

  • Refine by Publication Year
  • 2 2025
  • 1 2013
  • 2 2006

  • Refine by Author
  • 3 Hildebrandt, Andreas
  • 1 Althaus, Ernst
  • 1 Berger, Peter
  • 1 Cauchard, Jessica R.
  • 1 Fernet, Laouen
  • Show More...

  • Refine by Series/Journal
  • 1 LIPIcs
  • 2 OASIcs
  • 2 DagSemProc

  • Refine by Classification
  • 1 Computer systems organization → External interfaces for robotics
  • 1 Computing methodologies → Distributed algorithms
  • 1 Human-centered computing → HCI theory, concepts and models
  • 1 Human-centered computing → Interaction paradigms
  • 1 Security and privacy → Logic and verification
  • Show More...

  • Refine by Keyword
  • 2 Mass spectrometry
  • 1 Isabelle/HOL
  • 1 Liquid chromatography
  • 1 TMT labeling
  • 1 Top-down Proteomics
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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