| 1. |
- Happonen, Lotta, et al.
(författare)
-
A quantitative Streptococcus pyogenes-human protein-protein interaction map reveals localization of opsonizing antibodies
- 2019
-
Ingår i: Nature Communications. - : Springer Science and Business Media LLC. - 2041-1723. ; 10:1, s. 2727-2727
-
Tidskriftsartikel (refereegranskat)abstract
- A fundamental challenge in medical microbiology is to characterize the dynamic protein-protein interaction networks formed at the host-pathogen interface. Here, we generate a quantitative interaction map between the significant human pathogen, Streptococcus pyogenes, and proteins from human saliva and plasma obtained via complementary affinity-purification and bacterial-surface centered enrichment strategies and quantitative mass spectrometry. Perturbation of the network using immunoglobulin protease cleavage, mixtures of different concentrations of saliva and plasma, and different S. pyogenes serotypes and their isogenic mutants, reveals how changing microenvironments alter the interconnectivity of the interaction map. The importance of host immunoglobulins for the interaction with human complement proteins is demonstrated and potential protective epitopes of importance for phagocytosis of S. pyogenes cells are localized. The interaction map confirms several previously described protein-protein interactions; however, it also reveals a multitude of additional interactions, with possible implications for host-pathogen interactions involving other bacterial species.
|
|
| 2. |
- Birkedal, Lars, et al.
(författare)
-
Guarded Cubical Type Theory
- 2019
-
Ingår i: Journal of Automated Reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 63:2, s. 211-253
-
Tidskriftsartikel (refereegranskat)abstract
- This paper improves the treatment of equality in guarded dependent type theory ((Formula presented.)), by combining it with cubical type theory ((Formula presented.)). (Formula presented.) is an extensional type theory with guarded recursive types, which are useful for building models of program logics, and for programming and reasoning with coinductive types. We wish to implement (Formula presented.) with decidable type checking, while still supporting non-trivial equality proofs that reason about the extensions of guarded recursive constructions. (Formula presented.) is a variation of Martin–Löf type theory in which the identity type is replaced by abstract paths between terms. (Formula presented.) provides a computational interpretation of functional extensionality, enjoys canonicity for the natural numbers type, and is conjectured to support decidable type-checking. Our new type theory, guarded cubical type theory ((Formula presented.)), provides a computational interpretation of extensionality for guarded recursive types. This further expands the foundations of (Formula presented.) as a basis for formalisation in mathematics and computer science. We present examples to demonstrate the expressivity of our type theory, all of which have been checked using a prototype type-checker implementation. We show that (Formula presented.) can be given semantics in presheaves on (Formula presented.), where (Formula presented.) is the cube category, and (Formula presented.) is any small category with an initial object. We then show that the category of presheaves on (Formula presented.) provides semantics for (Formula presented.).
|
|
| 3. |
- Birkedal, Lars, et al.
(författare)
-
Guarded Cubical Type Theory: Path Equality for Guarded Recursion
- 2016
-
Ingår i: Leibniz International Proceedings in Informatics, LIPIcs. - 1868-8969. - 9783959770224 ; 62, s. 23:1-23:17
-
Konferensbidrag (refereegranskat)abstract
- This paper improves the treatment of equality in guarded dependent type theory (GDTT), by combining it with cubical type theory (CTT). GDTT is an extensional type theory with guarded recursive types, which are useful for building models of program logics, and for programming and reasoning with coinductive types. We wish to implement GDTT with decidable type checking, while still supporting non-trivial equality proofs that reason about the extensions of guarded recursive constructions. CTT is a variation of Martin-Löf type theory in which the identity type is replaced by abstract paths between terms. CTT provides a computational interpretation of functional extensionality, is conjectured to have decidable type checking, and has an implemented type checker. Our new type theory, called guarded cubical type theory, provides a computational interpretation of extensionality for guarded recursive types. This further expands the foundations of CTT as a basis for formalisation in mathematics and computer science. We present examples to demonstrate the expressivity of our type theory, all of which have been checked using a prototype type-checker implementation, and present semantics in a presheaf category.
|
|
| 4. |
- Malmström, Lars, et al.
(författare)
-
Quantitative proteogenomics of human pathogens using DIA-MS.
- 2015
-
Ingår i: Journal of Proteomics. - : Elsevier BV. - 1874-3919 .- 1876-7737. ; 129, s. 98-107
-
Tidskriftsartikel (refereegranskat)abstract
- The increasing number of bacterial genomes in combination with reproducible quantitative proteome measurements provides new opportunities to explore how genetic differences modulate proteome composition and virulence. It is challenging to combine genome and proteome data as the underlying genome influences the proteome. We present a strategy to facilitate the integration of genome data from several genetically similar bacterial strains with data-independent analysis mass spectrometry (DIA-MS) for rapid interrogation of the combined data sets. The strategy relies on the construction of a composite genome combining all genetic data in a compact format, which can accommodate the fusion with quantitative peptide and protein information determined via DIA-MS. We demonstrate the method by combining data sets from whole genome sequencing, shotgun MS and DIA-MS from 34 clinical isolates of Streptococcus pyogenes. The data structure allows for fast exploration of the data showing that undetected proteins are on average more amenable to amino acid substitution than expressed proteins. We identified several significantly differentially expressed proteins between invasive and non-invasive strains. The work underlines how integration of whole genome sequencing with accurately quantified proteomes can further advance the interpretation of the relationship between genomes, proteomes and virulence.
|
|
