4 Search Results for "Streicher, Thomas"

Document
DOI: 10.4230/LIPIcs.CALCO.2019.18
Nominal String Diagrams

Authors: Samuel Balco and Alexander Kurz

Published in: LIPIcs, Volume 139, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)

Abstract
We introduce nominal string diagrams as string diagrams internal in the category of nominal sets. This requires us to take nominal sets as a monoidal category, not with the cartesian product, but with the separated product. To this end, we develop the beginnings of a theory of monoidal categories internal in a symmetric monoidal category. As an instance, we obtain a notion of a nominal PROP as a PROP internal in nominal sets. A 2-dimensional calculus of simultaneous substitutions is an application.
Cite as

Samuel Balco and Alexander Kurz. Nominal String Diagrams. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 18:1-18:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{balco_et_al:LIPIcs.CALCO.2019.18,
  author =	{Balco, Samuel and Kurz, Alexander},
  title =	{{Nominal String Diagrams}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{18:1--18:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-120-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{139},
  editor =	{Roggenbach, Markus and Sokolova, Ana},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.18},
  URN =		{urn:nbn:de:0030-drops-114466},
  doi =		{10.4230/LIPIcs.CALCO.2019.18},
  annote =	{Keywords: string diagrams, nominal sets, separated product, simultaneous substitutions, internal category, monoidal category, internal monoidal categories, PROP}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2019.31
Cubical Syntax for Reflection-Free Extensional Equality

Authors: Jonathan Sterling, Carlo Angiuli, and Daniel Gratzer

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

Abstract
We contribute XTT, a cubical reconstruction of Observational Type Theory [Altenkirch et al., 2007] which extends Martin-Löf’s intensional type theory with a dependent equality type that enjoys function extensionality and a judgmental version of the unicity of identity proofs principle (UIP): any two elements of the same equality type are judgmentally equal. Moreover, we conjecture that the typing relation can be decided in a practical way. In this paper, we establish an algebraic canonicity theorem using a novel extension of the logical families or categorical gluing argument inspired by Coquand and Shulman [Coquand, 2018; Shulman, 2015]: every closed element of boolean type is derivably equal to either true or false.
Cite as

Jonathan Sterling, Carlo Angiuli, and Daniel Gratzer. Cubical Syntax for Reflection-Free Extensional Equality. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 31:1-31:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{sterling_et_al:LIPIcs.FSCD.2019.31,
  author =	{Sterling, Jonathan and Angiuli, Carlo and Gratzer, Daniel},
  title =	{{Cubical Syntax for Reflection-Free Extensional Equality}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{31:1--31:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.31},
  URN =		{urn:nbn:de:0030-drops-105387},
  doi =		{10.4230/LIPIcs.FSCD.2019.31},
  annote =	{Keywords: Dependent type theory, extensional equality, cubical type theory, categorical gluing, canonicity}
}
Document
DOI: 10.4230/LIPIcs.CSL.2011.470
Relative Completeness for Logics of Functional Programs

Authors: Bernhard Reus and Thomas Streicher

Published in: LIPIcs, Volume 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (2011)

Abstract
We prove a relative completeness result for a logic of functional programs extending D. Scott's LCF. For such a logic, contrary to results for Hoare logic, it does not make sense to ask whether it is complete relative to the full theory of its first-order part, since the first order part does not determine uniquely the model at higher-order types. Therefore, one has to fix a model and choose an appropriate data theory w.r.t. which the logic is relatively complete. We establish relative completeness for two models: for the Scott model we use the theory of Baire Space as data theory, and for the effective Scott model we take first-order arithmetic. In both cases we need to extend traditional LCF in order to capture a sufficient amount of domain theory.
Cite as

Bernhard Reus and Thomas Streicher. Relative Completeness for Logics of Functional Programs. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 470-480, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{reus_et_al:LIPIcs.CSL.2011.470,
  author =	{Reus, Bernhard and Streicher, Thomas},
  title =	{{Relative Completeness for Logics of Functional Programs}},
  booktitle =	{Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
  pages =	{470--480},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-32-3},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{12},
  editor =	{Bezem, Marc},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.470},
  URN =		{urn:nbn:de:0030-drops-32509},
  doi =		{10.4230/LIPIcs.CSL.2011.470},
  annote =	{Keywords: completeness, program logics, LCF}
}
Document
DOI: 10.4230/DagSemRep.303
Semantic Foundations of Proof-search (Dagstuhl Seminar 01141)

Authors: David Pym, Eike Ritter, and Thomas Streicher

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

David Pym, Eike Ritter, and Thomas Streicher. Semantic Foundations of Proof-search (Dagstuhl Seminar 01141). Dagstuhl Seminar Report 303, pp. 1-16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2001)

Copy BibTex To Clipboard

@TechReport{pym_et_al:DagSemRep.303,
  author =	{Pym, David and Ritter, Eike and Streicher, Thomas},
  title =	{{Semantic Foundations of Proof-search (Dagstuhl Seminar 01141)}},
  pages =	{1--16},
  ISSN =	{1619-0203},
  year =	{2001},
  type = 	{Dagstuhl Seminar Report},
  number =	{303},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemRep.303},
  URN =		{urn:nbn:de:0030-drops-151879},
  doi =		{10.4230/DagSemRep.303},
}
  • Refine by Author
  • 2 Streicher, Thomas
  • 1 Angiuli, Carlo
  • 1 Balco, Samuel
  • 1 Gratzer, Daniel
  • 1 Kurz, Alexander
  • Show More...

  • Refine by Classification
  • 1 Mathematics of computing
  • 1 Software and its engineering → General programming languages
  • 1 Theory of computation → Algebraic semantics
  • 1 Theory of computation → Denotational semantics
  • 1 Theory of computation → Logic
  • Show More...

  • Refine by Keyword
  • 1 Dependent type theory
  • 1 LCF
  • 1 PROP
  • 1 canonicity
  • 1 categorical gluing
  • Show More...

  • Refine by Type
  • 4 document

  • Refine by Publication Year
  • 2 2019
  • 1 2001
  • 1 2011

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