3 Search Results for "Morris, J. Garrett"


Document
Separating Sessions Smoothly

Authors: Simon Fowler, Wen Kokke, Ornela Dardha, Sam Lindley, and J. Garrett Morris

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)


Abstract
This paper introduces Hypersequent GV (HGV), a modular and extensible core calculus for functional programming with session types that enjoys deadlock freedom, confluence, and strong normalisation. HGV exploits hyper-environments, which are collections of type environments, to ensure that structural congruence is type preserving. As a consequence we obtain a tight operational correspondence between HGV and HCP, a hypersequent-based process-calculus interpretation of classical linear logic. Our translations from HGV to HCP and vice-versa both preserve and reflect reduction. HGV scales smoothly to support Girard’s Mix rule, a crucial ingredient for channel forwarding and exceptions.

Cite as

Simon Fowler, Wen Kokke, Ornela Dardha, Sam Lindley, and J. Garrett Morris. Separating Sessions Smoothly. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 36:1-36:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{fowler_et_al:LIPIcs.CONCUR.2021.36,
  author =	{Fowler, Simon and Kokke, Wen and Dardha, Ornela and Lindley, Sam and Morris, J. Garrett},
  title =	{{Separating Sessions Smoothly}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{36:1--36:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.36},
  URN =		{urn:nbn:de:0030-drops-144138},
  doi =		{10.4230/LIPIcs.CONCUR.2021.36},
  annote =	{Keywords: session types, hypersequents, linear lambda calculus}
}
Document
Mixed Messages: Measuring Conformance and Non-Interference in TypeScript (Artifact)

Authors: Jack Williams, J. Garrett Morris, Philip Wadler, and Jakub Zalewski

Published in: DARTS, Volume 3, Issue 2, Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017)


Abstract
In the paper Mixed Messages: Measuring Conformance and Non-Interference in TypeScript we present our experiences of evaluating gradual typing using our tool TypeScript TPD. The tool, based on the polymorphic blame calculus, monitors JavaScript libraries and TypeScript clients against the corresponding TypeScript definition. Our experiments yield two conclusions. First, TypeScript definitions are prone to error. Second, there are serious technical concerns with the use of the JavaScript proxy mechanism for enforcing contracts. This artifact includes all the libraries we tested, their definition files, and the source code of our tool. From this, all libraries can be wrapped and tested to reproduce the log data that formed our conclusion. All conformance errors and examples of interference are documented, and can be verified against the generated logs.

Cite as

Jack Williams, J. Garrett Morris, Philip Wadler, and Jakub Zalewski. Mixed Messages: Measuring Conformance and Non-Interference in TypeScript (Artifact). In Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017). Dagstuhl Artifacts Series (DARTS), Volume 3, Issue 2, pp. 8:1-8:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@Article{williams_et_al:DARTS.3.2.8,
  author =	{Williams, Jack and Morris, J. Garrett and Wadler, Philip and Zalewski, Jakub},
  title =	{{Mixed Messages: Measuring Conformance and Non-Interference in TypeScript (Artifact)}},
  pages =	{8:1--8:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2017},
  volume =	{3},
  number =	{2},
  editor =	{Williams, Jack and Morris, J. Garrett and Wadler, Philip and Zalewski, Jakub},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.3.2.8},
  URN =		{urn:nbn:de:0030-drops-72899},
  doi =		{10.4230/DARTS.3.2.8},
  annote =	{Keywords: gradual typing, TypeScript, JavaScript, proxies}
}
Document
Mixed Messages: Measuring Conformance and Non-Interference in TypeScript

Authors: Jack Williams, J. Garrett Morris, Philip Wadler, and Jakub Zalewski

Published in: LIPIcs, Volume 74, 31st European Conference on Object-Oriented Programming (ECOOP 2017)


Abstract
TypeScript participates in the recent trend among programming languages to support gradual typing. The DefinitelyTyped Repository for TypeScript supplies type definitions for over 2000 popular JavaScript libraries. However, there is no guarantee that implementations conform to their corresponding declarations. We present a practical evaluation of gradual typing for TypeScript. We have developed a tool for use with TypeScript, based on the polymorphic blame calculus, for monitoring JavaScript libraries and TypeScript clients against the TypeScript definition. We apply our tool, TypeScript TPD, to those libraries in the DefinitelyTyped Repository which had adequate test code to use. Of the 122 libraries we checked, 62 had cases where either the library or its tests failed to conform to the declaration. Gradual typing should satisfy non-interference. Monitoring a program should never change its behaviour, except to raise a type error should a value not conform to its declared type. However, our experience also suggests serious technical concerns with the use of the JavaScript proxy mechanism for enforcing contracts. Of the 122 libraries we checked, 22 had cases where the library or its tests violated non-interference.

Cite as

Jack Williams, J. Garrett Morris, Philip Wadler, and Jakub Zalewski. Mixed Messages: Measuring Conformance and Non-Interference in TypeScript. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 28:1-28:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{williams_et_al:LIPIcs.ECOOP.2017.28,
  author =	{Williams, Jack and Morris, J. Garrett and Wadler, Philip and Zalewski, Jakub},
  title =	{{Mixed Messages: Measuring Conformance and Non-Interference in TypeScript}},
  booktitle =	{31st European Conference on Object-Oriented Programming (ECOOP 2017)},
  pages =	{28:1--28:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-035-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{74},
  editor =	{M\"{u}ller, Peter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.28},
  URN =		{urn:nbn:de:0030-drops-72640},
  doi =		{10.4230/LIPIcs.ECOOP.2017.28},
  annote =	{Keywords: Gradual Typing, TypeScript, JavaScript, Proxies}
}
  • Refine by Author
  • 3 Morris, J. Garrett
  • 2 Wadler, Philip
  • 2 Williams, Jack
  • 2 Zalewski, Jakub
  • 1 Dardha, Ornela
  • Show More...

  • Refine by Classification
  • 1 Software and its engineering → Functional languages
  • 1 Theory of computation → Linear logic

  • Refine by Keyword
  • 2 JavaScript
  • 2 TypeScript
  • 1 Gradual Typing
  • 1 Proxies
  • 1 gradual typing
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 2 2017
  • 1 2021

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