Semantic Structures for Higher-Order Information Flow

Research output

Research output per year 2010 2010 2011 2013 2016 2020

• 10 Chapter in a published conference proceeding
• 10 Article
• 4 Chapter or section
• 1 Paper
• 1 More
  • 1 Conference article

Research output per year

Research output per year

Search results

• 2020

  A Curry-style Semantics of Interaction: From Untyped to Second-Order Lazy λμ-Calculus

  Laird, J., 2020, Foundations of Software Science and Computation Structures- 23rd International Conference, FOSSACS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings. Goubault-Larrecq, J. & König, B. (eds.). Cham, Switzerland: Springer, p. 422-441 20 p. (Lecture Notes in Computer Science ; vol. 12077).

  Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

  Open Access

  File

  • Abstract Machine 100%
  • Polymorphic Type 100%
  • Transition System 100%
  • Control Flow 100%
  • Parallel Composition 100%
  90 Downloads (Pure)

• Weighted models for higher-order computation

  Laird, J., 31 Dec 2020, In: Information and Computation. 275, 104645.

  Research output: Contribution to journal › Article › peer-review

  Open Access

  File

  • Game Semantics 100%
  • Functor 100%
  • Multiset 100%
  • Fixed Points 100%
  • Biproduct 100%
  3 Citations (SciVal)

  58 Downloads (Pure)
• 2019

  From Global to Local State, Coalgebraically and Compositionally

  Laird, J., 30 Nov 2019, In: Electronic Notes in Theoretical Computer Science. 347, p. 203-222 20 p.

  Research output: Contribution to journal › Conference article › peer-review

  Open Access

  • And-States 100%
  • coalgebra 33%
  • Equational Theory 33%
  • Categorical Semantics 33%
  • Type Constructor 33%
  1 Citation (SciVal)
• 2018

  A fully abstract game semantics for countable nondeterminism

  Gowers, W. J. & Laird, J. D., 1 Aug 2018, Computer Science Logic 2018, CSL 2018. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, Vol. 119. 24

  Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

  Open Access

  • Nondeterminism 100%
  • Concurrent Program 14%
  1 Citation (SciVal)

• Extensional and intensional semantic universes: A denotational model of dependent types

  Blot, V. & Laird, J., 31 Jul 2018, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018. IEEE, Vol. Part F138033. p. 95-104 10 p. (Proceedings - Symposium on Logic in Computer Science).

  Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

  Open Access

  • Type Theory 100%
  • Dependent Type 100%
  • Data Structure 100%
  • Programming Language 50%
  • Operational Semantics 50%
  1 Citation (SciVal)

  12 Downloads (Pure)
• 2017

  Combining Control Effects and Their Models: Game Semantics for a hierarchy of static, dynamic and delimited control effects.

  Laird, J., 28 Feb 2017, In: Annals of Pure and Applied Logic. 168, 2, p. 470-500 31 p.

  Research output: Contribution to journal › Article › peer-review

  Open Access

  • Annotation 100%
  • Operational Semantics 100%
  • Denotational Semantics 100%
  • Control Flow 100%
  • Control Operator 100%
  2 Citations (SciVal)

• Realizability for Peano arithmetic with winning conditions in HON games

  Blot, V., 1 Feb 2017, In: Annals of Pure and Applied Logic. 168, 2, p. 254-277 24 p.

  Research output: Contribution to journal › Article › peer-review

  Open Access

  • Winning Strategy 100%
  2 Citations (SciVal)
• 2016

  Classical extraction in continuation models

  Blot, V., 1 Jun 2016, Leibniz International Proceedings in Informatics, LIPIcs, 2016. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, Vol. 52. p. 13.1-13.17 17 p. 13

  Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

  Open Access

  • Game Semantics 100%
  • Classical Theory 100%
  • Natural Number 100%
  • Main Difference 100%
  • Distinct Object 100%

• Fixed points in quantitative semantics

  Laird, J., 5 Jul 2016, LICS '16, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science . Shankar, N. (ed.). New York, U. S. A.: Association for Computing Machinery, p. 347-356 10 p. (Proceedings - Symposium on Logic in Computer Science).

  Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

  Open Access

  File

  • Fixed Points 100%
  • Monoids 20%
  • Theoretic Structure 20%
  • Multiset 20%
  • Morphism 20%
  10 Citations (SciVal)

  303 Downloads (Pure)

• Hybrid realizability for intuitionistic and classical choice

  Blot, V., 5 Jul 2016, LICS '16, Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science. New York, U. S. A.: IEEE, p. 575-584 10 p.

  Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

  • Classical Logic 100%
  • Axiom of Choice 100%
  • Type Theory 33%
  • Computable Function 33%
  • Provability 33%
  3 Citations (SciVal)

• Polymorphic Game Semantics for Dynamic Binding

  Laird, J., 1 Sept 2016.

  Research output: Contribution to conference › Paper › peer-review

  Open Access

  • Dynamic Binding 100%
  • Structured Block 66%

• Weighted relational models for mobility

  Laird, J., 1 Jun 2016, Leibniz International Proceedings in Informatics, LIPIcs. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, Vol. 52. p. 1-15 15 p. 24

  Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

  Open Access

  • Relational Database 100%
  • Denotational Semantics 100%
  • Calculus 100%
  • Observational Equivalence 50%
  • Operational Semantics 50%
• 2015

  Sequential algorithms for unbounded nondeterminism

  Laird, J., 21 Dec 2015, In: Electronic Notes in Theoretical Computer Science. 319, p. 271-287 17 p.

  Research output: Contribution to journal › Article › peer-review

  Open Access

  • Nondeterminism 100%
  • Sequential Algorithm 100%
  • Monotone Function 66%
  • Functional Languages 33%
  • Functional Program 33%
  3 Citations (SciVal)

  83 Downloads (Pure)

• Typed realizability for first-order classical analysis

  Blot, V., 31 Dec 2015, In: Logical Methods in Computer Science. 11, 4

  Research output: Contribution to journal › Article › peer-review

  Open Access

  • Intuitionistic Logic 100%
  • Computational Modeling 100%
  • Relativization 100%
  • Calculus 100%
  2 Citations (SciVal)
• 2013

  Combining and relating control effects and their semantics

  Laird, J., 5 Sept 2013, In: EPTCS.

  Research output: Contribution to journal › Article › peer-review

  • Control Flow 100%
  • Soundness 50%
  • Programming Language 50%
  • Explicit Representation 50%
  • Control-Flow Analysis 50%

• Constructing differential categories and deconstructing categories of games

  Laird, J., Manzonetto, G. & McCusker, G., Jan 2013, In: Information and Computation. 222, p. 247-264 18 p.

  Research output: Contribution to journal › Article › peer-review

  Open Access

  File

  • Calculus 100%
  • Definability 100%
  • Differential Operator 100%
  • Combinator 100%
  • Imperative Language 100%
  16 Citations (SciVal)

  249 Downloads (Pure)

• Game semantics for a polymorphic programming language

  Laird, J., Aug 2013, In: Journal of the ACM. 60, 4, 27 p., 29.

  Research output: Contribution to journal › Article › peer-review

  Open Access

  File

  • Programming Language 100%
  • Instantiation 50%
  • Positive Occurrence 50%
  • Answer Question 50%
  • Negative Occurrence 50%
  11 Citations (SciVal)

  199 Downloads (Pure)

• Imperative programs as proofs via game semantics

  Churchill, M., Laird, J. & McCusker, G., Nov 2013, In: Annals of Pure and Applied Logic. 164, 11, p. 1038-1078 41 p.

  Research output: Contribution to journal › Article › peer-review

  Open Access

  File

  • Programming Language 100%
  • lambda-calculus 100%
  • Intuitionistic Logic 100%
  • Proof System 100%
  • Winning Strategy 100%
  3 Citations (SciVal)

  182 Downloads (Pure)

• Weighted relational models of typed Lambda-Calculi

  Laird, J. D., Manzonetto, G., Mccusker, G. & Pagani, M., 1 Jun 2013, 2013 28th Annual IEEE/ACM Symposium on Logic in Computer Science (LICS). Los Alamitos, California: IEEE, p. 301-310 10 p. (Annual IEEE/ACM Symposium on Logic in Computer Science (LICS)).

  Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

  Open Access

  File

  • Calculus 100%
  • Linear Logic 100%
  • lambda-calculus 100%
  • Relational Database 100%
  • Denotational Semantics 100%
  63 Citations (SciVal)

  375 Downloads (Pure)
• 2011

  Constructing differential categories and deconstructing categories of games

  Laird, J., Manzonetto, G. & McCusker, G., 2011, Automata, Languages and Programming - 38th International Colloquium, ICALP 2011, Proceedings. Aceto, L., Henzinger, M. & Sgall, J. (eds.). Heidelberg, Germany: Springer, p. 186-197 12 p. (Lecture Notes in Computer Science; vol. 6756).

  Research output: Chapter or section in a book/report/conference proceeding › Chapter or section

  Open Access

  File

  • Imperative Language 100%
  • Resource Model 100%
  • Relational Semantics 100%
  • Calculus 100%
  • Apply It 100%
  5 Citations (SciVal)

  159 Downloads (Pure)

• Imperative programs as proofs via game semantics

  Churchill, M., Laird, J. & McCusker, G., 2011, 26th Annual IEEE Symposium on Logic in Computer Science (LICS) 2011. IEEE, p. 65-74 10 p. (Annual Symposium on Logic in Computer Science).

  Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

  File

  • Programming Language 100%
  • lambda-calculus 100%
  • Intuitionistic Logic 100%
  4 Citations (SciVal)

  254 Downloads (Pure)

• Isomorphisms of types in the presence of higher-order references

  Clairambault, P., 2011, 2011 IEEE 26th Annual Symposium on Logic in Computer Science. Piscataway, NJ: IEEE, p. 152-161 10 p.

  Research output: Chapter or section in a book/report/conference proceeding › Chapter or section

  • Programming Language 100%
  • Renaming 100%
  • Equational Theory 100%
  • Theoretic Model 100%
  • Open Problem 100%
  2 Citations (SciVal)

• The biequivalence of locally cartesian closed categories and martin-löf type theories

  Clairambault, P. & Dybjer, P., 2011, Typed Lambda Calculi and Applications - 10th International Conference, TLCA 2011, Proceedings. Heidelberg: Springer, Vol. 6690 LNCS. p. 91-106 16 p. (Lecture Notes in Computer Science).

  Research output: Chapter or section in a book/report/conference proceeding › Chapter or section

  • Type Theory 100%
  • Category Theory 16%
  • Corrected Version 16%
  • Pullback 16%
  15 Citations (SciVal)
• 2010

  A logic of sequentiality

  Churchill, M. & Laird, J., 24 Aug 2010, Computer Science Logic (Lecture Notes in Computer Science). Dawar, A. & Veith, H. (eds.). Springer, Vol. 6247/2. p. 215-229 15 p. (Lecture Notes in Computer Science).

  Research output: Chapter or section in a book/report/conference proceeding › Chapter or section

  File

  • Functional Program 100%
  6 Citations (SciVal)

  115 Downloads (Pure)

• Game semantics for a polymorphic programming language

  Laird, J., 2010, 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010. IEEE, p. 41-49 9 p. (Proceedings - Symposium on Logic in Computer Science).

  Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

  • Programming Language 100%
  • And-States 50%
  • Instantiation 50%
  • Positive Occurrence 50%
  • Model Checking 50%
  7 Citations (SciVal)

• Game semantics for call-by-value polymorphism

  Laird, J., Jul 2010, In: Lecture Notes in Computer Science. 6199 LNCS, p. 187-198 12 p.

  Research output: Contribution to journal › Article

  • Call by Value 100%
  • Instantiation 33%
  • Model Checking 33%
  • Checking Technique 33%
  • Polymorphic Type 33%
  4 Citations (SciVal)