4 Search Results for "Vicary, Jamie"


Document
Sheaf Semantics of Termination-Insensitive Noninterference

Authors: Jonathan Sterling and Robert Harper

Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)


Abstract
We propose a new sheaf semantics for secure information flow over a space of abstract behaviors, based on synthetic domain theory: security classes are open/closed partitions, types are sheaves, and redaction of sensitive information corresponds to restricting a sheaf to a closed subspace. Our security-aware computational model satisfies termination-insensitive noninterference automatically, and therefore constitutes an intrinsic alternative to state of the art extrinsic/relational models of noninterference. Our semantics is the latest application of Sterling and Harper’s recent re-interpretation of phase distinctions and noninterference in programming languages in terms of Artin gluing and topos-theoretic open/closed modalities. Prior applications include parametricity for ML modules, the proof of normalization for cubical type theory by Sterling and Angiuli, and the cost-aware logical framework of Niu et al. In this paper we employ the phase distinction perspective twice: first to reconstruct the syntax and semantics of secure information flow as a lattice of phase distinctions between "higher" and "lower" security, and second to verify the computational adequacy of our sheaf semantics with respect to a version of Abadi et al.’s dependency core calculus to which we have added a construct for declassifying termination channels.

Cite as

Jonathan Sterling and Robert Harper. Sheaf Semantics of Termination-Insensitive Noninterference. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{sterling_et_al:LIPIcs.FSCD.2022.5,
  author =	{Sterling, Jonathan and Harper, Robert},
  title =	{{Sheaf Semantics of Termination-Insensitive Noninterference}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{5:1--5:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-233-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{228},
  editor =	{Felty, Amy P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.5},
  URN =		{urn:nbn:de:0030-drops-162869},
  doi =		{10.4230/LIPIcs.FSCD.2022.5},
  annote =	{Keywords: information flow, noninterference, denotational semantics, phase distinction, Artin gluing, modal type theory, topos theory, synthetic domain theory, synthetic Tait computability}
}
Document
A Classical Groupoid Model for Quantum Networks

Authors: David Reutter and Jamie Vicary

Published in: LIPIcs, Volume 72, 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)


Abstract
We give a mathematical analysis of a new type of classical computer network architecture, intended as a model of a new technology that has recently been proposed in industry. Our approach is based on groubits, generalizations of classical bits based on groupoids. This network architecture allows the direct execution of a number of protocols that are usually associated with quantum networks, including teleportation, dense coding and secure key distribution.

Cite as

David Reutter and Jamie Vicary. A Classical Groupoid Model for Quantum Networks. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 19:1-19:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{reutter_et_al:LIPIcs.CALCO.2017.19,
  author =	{Reutter, David and Vicary, Jamie},
  title =	{{A Classical Groupoid Model for Quantum Networks}},
  booktitle =	{7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
  pages =	{19:1--19:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-033-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{72},
  editor =	{Bonchi, Filippo and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2017.19},
  URN =		{urn:nbn:de:0030-drops-80391},
  doi =		{10.4230/LIPIcs.CALCO.2017.19},
  annote =	{Keywords: groupoids, networks, quantum, semantics, key distribution}
}
Document
A 2-Categorical Approach to Composing Quantum Structures

Authors: David Reutter and Jamie Vicary

Published in: LIPIcs, Volume 72, 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)


Abstract
We present an infinite number of construction schemes for quantum structures, including unitary error bases, Hadamard matrices, quantum Latin squares and controlled families, many of which have not previously been described. Our results rely on the type structure of biunitary connections, 2-categorical structures which play a central role in the theory of planar algebras. They have an attractive graphical calculus which allows simple correctness proofs for the constructions we present. We apply these techniques to construct a unitary error basis that cannot be built using any previously known method.

Cite as

David Reutter and Jamie Vicary. A 2-Categorical Approach to Composing Quantum Structures. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 20:1-20:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{reutter_et_al:LIPIcs.CALCO.2017.20,
  author =	{Reutter, David and Vicary, Jamie},
  title =	{{A 2-Categorical Approach to Composing Quantum Structures}},
  booktitle =	{7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
  pages =	{20:1--20:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-033-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{72},
  editor =	{Bonchi, Filippo and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2017.20},
  URN =		{urn:nbn:de:0030-drops-80389},
  doi =		{10.4230/LIPIcs.CALCO.2017.20},
  annote =	{Keywords: quantum constructions, 2-category, graphical calculus, planar algebra}
}
Document
Globular: An Online Proof Assistant for Higher-Dimensional Rewriting

Authors: Krzysztof Bar, Aleks Kissinger, and Jamie Vicary

Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)


Abstract
This article introduces Globular, an online proof assistant for the formalization and verification of proofs in higher-dimensional category theory. The tool produces graphical visualizations of higher-dimensional proofs, assists in their construction with a point-and-click interface, and performs type checking to prevent incorrect rewrites. Hosted on the web, it has a low barrier to use, and allows hyperlinking of formalized proofs directly from research papers. It allows the formalization of proofs from logic, topology and algebra which are not formalizable by other methods, and we give several examples.

Cite as

Krzysztof Bar, Aleks Kissinger, and Jamie Vicary. Globular: An Online Proof Assistant for Higher-Dimensional Rewriting. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 34:1-34:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{bar_et_al:LIPIcs.FSCD.2016.34,
  author =	{Bar, Krzysztof and Kissinger, Aleks and Vicary, Jamie},
  title =	{{Globular: An Online Proof Assistant for Higher-Dimensional Rewriting}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{34:1--34:11},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.34},
  URN =		{urn:nbn:de:0030-drops-59880},
  doi =		{10.4230/LIPIcs.FSCD.2016.34},
  annote =	{Keywords: higher category theory, higher-dimensional rewriting, interactive theorem proving}
}
  • Refine by Author
  • 3 Vicary, Jamie
  • 2 Reutter, David
  • 1 Bar, Krzysztof
  • 1 Harper, Robert
  • 1 Kissinger, Aleks
  • Show More...

  • Refine by Classification
  • 1 Security and privacy → Formal methods and theory of security
  • 1 Theory of computation → Abstraction
  • 1 Theory of computation → Categorical semantics
  • 1 Theory of computation → Denotational semantics
  • 1 Theory of computation → Type theory

  • Refine by Keyword
  • 1 2-category
  • 1 Artin gluing
  • 1 denotational semantics
  • 1 graphical calculus
  • 1 groupoids
  • Show More...

  • Refine by Type
  • 4 document

  • Refine by Publication Year
  • 2 2017
  • 1 2016
  • 1 2022

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