Browse by Author or creator

2024

Atkey, Robert and Kokke, Wen (2024) A semantic proof of generalised cut elimination for deep inference. Electronic Notes in Theoretical Informatics and Computer Science, 4. ISSN 2969-2431

Atkey, Robert (2024) Polynomial time and dependent types. Proceedings of the ACM on Programming Languages (PACMPL), 8 (POPL). 2288–2317. 76. ISSN 2475-1421

2023

Daggitt, Matthew L. and Atkey, Robert and Kokke, Wen and Komendantskaya, Ekaterina and Arnaboldi, Luca; Krebbers, Robbert and Traytel, Dmitriy and Pientka, Brigitte and Zdancewic, Steve, eds. (2023) Compiling higher-order specifications to SMT solvers : how to deal with rejection constructively. In: CPP 2023 : Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs. ACM, New York, NY., pp. 102-120. ISBN 9798400700262

2022

Wood, James and Atkey, Robert; (2022) A framework for substructural type systems. In: ESOP 2022 Proceedings. Lecture Notes in Computer Science . Springer, DEU.

2021

Wood, James and Atkey, Robert (2021) A linear algebra approach to linear metatheory. Electronic Proceedings in Theoretical Computer Science, EPTCS, 354 (2021). pp. 195-212. ISSN 2075-2180

Allais, Guillaume and Atkey, Robert and Chapman, James and McBride, Conor and McKinna, James (2021) A type and scope safe universe of syntaxes with binding : their semantics and proofs. Journal of Functional Programming, 31. e22. ISSN 0956-7968

2020

Kokke, Wen and Komendantskaya, Ekaterina and Kienitz, Daniel and Atkey, Bob and Aspinall, David (2020) Neural networks, secure by construction : an exploration of refinement types. In: The 18th Asian Symposium on Programming Languages and Systems, 2020-11-29 - 2020-12-03, Online.

Atkey, Robert and Gavranović, Bruno and Ghani, Neil and Kupke, Clemens and Ledent, Jérémy and Nordvall Forsberg, Fredrik (2020) Compositional Game Theory, compositionally. In: Applied Category Theory 2020, 2020-07-06 - 2020-07-10.

Hillerström, Daniel and Lindley, Sam and Atkey, Bob (2020) Effect handlers via generalised continuations. Journal of Functional Programming, 30. e5. ISSN 0956-7968

2019

Maillard, Kenji and Ahman, Danel and Atkey, Robert and Martínez, Guido and Hritcu, Catalin and Rivas, Exequiel and Tanter, Éric (2019) Dijkstra monads for all. Proceedings of the ACM on Programming Languages (PACMPL), 3 (ICFP). 104. ISSN 2475-1421

2018

Atkey, Bob and Wood, James (2018) Context constrained computation. In: 3rd Workshop on Type-Driven Development (TyDe '18), 2018-09-27 - 2018-09-27.

Allais, Guillaume and Atkey, Robert and Chapman, James and McBride, Conor and McKinna, James (2018) A type and scope safe universe of syntaxes with binding : their semantics and proofs. Proceedings of the ACM on Programming Languages (PACMPL), 2 (ICFP). pp. 1-30. 90. ISSN 2475-1421

Atkey, Robert; (2018) The syntax and semantics of quantitative type theory. In: LICS '18. ACM, New York, pp. 56-65. ISBN 978-1-4503-5583-4

2017

Hillerström, Daniel and Lindley, Sam and Atkey, Robert and Sivaramakrishnan, KC; Miller, Dale, ed. (2017) Continuation passing style for effect handlers. In: 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs) . Dagstuhl Publishing, Germany, 18:1-18:19.

Atkey, Robert; Yang, Hongseok, ed. (2017) Observed communication semantics for classical processes. In: Programming Languages and Systems. Lecture Notes in Computer Science . Springer, SWE, pp. 56-82.

2016

Atkey, Robert and Lindley, Sam and Morris, J. Garrett; Lindley, Sam and McBride, Conor and Trinder, Phil and Sannella, Don, eds. (2016) Conflation confers concurrency. In: A List of Successes That Can Change the World. Lecture Notes in Computer Science, 9600 . Springer, pp. 32-55. ISBN 9783319309354

2015

Atkey, Robert and Sannella, Donald (2015) ThreadSafe : static analysis for Java concurrency. Electronic Communications of the EASST, 72. ISSN 1863-2122

Atkey, Robert and Johann, Patricia (2015) Interleaving data and effects. Journal of Functional Programming, 25. e20. ISSN 0956-7968

Atkey, Robert and Ghani, Neil and Nordvall Forsberg, Fredrik and Revell, Timothy and Staton, Sam; Altenkirch, Thorsten, ed. (2015) Models for polymorphism over physical dimensions. In: 13th International Conference on Typed Lambda Calculi and Applications (TLCA'15). Leibniz International Proceedings in Informatics (LIPIcs) . Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, POL, pp. 999-1013.

2014

Atkey, Robert and Ghani, Neil and Johann, Patricia; (2014) A relationally parametric model of dependent type theory. In: POPL '14 Proceedings of the 41st ACM SIGPLAN-SIGACT. ACM, USA, pp. 503-515. ISBN 9781450325448

Atkey, Robert; Sewell, Peter, ed. (2014) From parametricity to conservation laws, via Noether's Theorem. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, USA, pp. 491-502. ISBN 9781450325448

2013

Atkey, Robert and McBride, Conor; (2013) Productive coprogramming with guarded recursion. In: Proceedings of the 2013 ACM SIGPLAN International Conference on Functional Programming. ACM, New York, NY. (In Press)

Atkey, Robert and Johann, Patricia and Kennedy, Andrew; Giacobazzi, Roberto and Cousot, Radhia, eds. (2013) Abstraction and invariance for algebraically indexed types. In: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. ACM Press, GBR, pp. 87-100. ISBN 9781450318327

2012

Atkey, Robert and Johann, Patricia and Ghani, Neil (2012) Refining inductive types. Logical Methods in Computer Science, 8 (2). 9. ISSN 1860-5974

Atkey, Robert and Ghani, Neil and Jacobs, Bart and Johann, Patricia; Birkedal, Lars, ed. (2012) Fibrational induction meets effects. In: Foundations of Software Science and Computational Structures. Lecture Notes in Computer Science, 7213 . Springer, EST, pp. 42-57.

Atkey, Robert; (2012) Relational parametricity for higher kinds. In: Computer science logic. EPTCS . UNSPECIFIED. (In Press)

Atkey, Robert; Dershowitz, Nachum, ed. (2012) The semantics of parsing with semantic actions. In: Proceedings of the Twenty-Seventh Annual ACM/IEEE Symposium on Logic In Computer Science (LICS 2012). UNSPECIFIED. (In Press)

2011

Atkey, Robert (2011) Amortised resource analysis with separation logic. Logical Methods in Computer Science, 7 (2). 17.

Atkey, Robert (2011) What is a categorical model of arrows? Electronic Notes in Theoretical Computer Science, 229 (5). pp. 19-37. ISSN 1571-0661

Atkey, Robert and Johann, Patricia and Ghani, Neil; Hofmann, Martin, ed. (2011) When is a type refinement an inductive type. In: Foundations of Software Science and Computational Structures. Lecture Notes in Computer Science . Springer, pp. 72-87. ISBN 978-3-642-19804-5

2010

Atkey, Robert; Gordon, Andrew, ed. (2010) Amortised resource analysis with separation logic. In: Proceedings of 19th European Symposium on Programming, ESOP 2010. Lecture Notes in Computer Science, 6012 . Springer, pp. 85-103.

Aspinall, David and Atkey, Robert and MacKenzie, Kenneth and Sannella, Donald; Wirsing, Martin and Hofmann, Martin and Rauschmayer, Axel, eds. (2010) Symbolic and analytic techniques for resource analysis of Java bytecode. In: Trustworthly Global Computing - 5th International Symposium, TGC 2010, Munich, Germany, February 24-26, 2010, Revised Selected Papers. Lecture Notes in Computer Science, 6084 . Springer, pp. 1-22. ISBN 9783642156397

2009

Atkey, Bob (2009) A deep embedding of parametric polymorphism in Coq. In: 4rd Informal ACM SIGPLAN Workshop on Mechanizing Metatheory, 2009-09-04.

Atkey, Robert (2009) Parameterised notions of computation. Journal of Functional Programming, 19 (3-4). pp. 335-376. ISSN 0956-7968

Atkey, Robert; Lenisa, Marina and Tarlecki, Andrzej, eds. (2009) Algebras for parameterised monads. In: Algebra and Coalgebra in Computer Science, Third International Conference, CALCO 2009. Lecture Notes in Computer Science, 5728 . Springer, pp. 3-17.

Atkey, Robert; Curien, Pierre-Louis, ed. (2009) Syntax for free: representing syntax with binding using parametricity. In: Typed Lambda Calculi and Applications, 9th International Conference, TLCA 2009. Lecture Notes in Computer Science, 5608 . Springer, pp. 35-49. ISBN 978-3-642-02272-2

Atkey, Robert and Lindley, Sam and Yallop, Jeremy; Weirich, Stephanie, ed. (2009) Unembedding domain-specific languages. In: Haskell '09 Proceedings of the 2nd ACM SIGPLAN Symposium on Haskell. ACM Press, GBR, pp. 37-48. ISBN 978-1-60558-508-6

2008

Atkey, Robert; (2008) CoqJVM : an executable specification of the Java Virtual Machine using dependent types. In: Types for Proofs and Programs (TYPES 2007). Lecture Notes in Computer Science, 4941 . Springer, [Berlin], pp. 18-33. ISBN 9783540681038

2006

Atkey, Robert; (2006) Parameterised notions of computation. In: Workshop on Mathematically Structured Functional Programming (MSFP 2006) (MSFP). Electronic Workshops in Computing . British Computer Society, London, pp. 1-15.

Atkey, Robert (2006) Specifying and verifying heap space allocation with JML and ESC/Java2. In: Formal Techniques for Java-like Programs, 2006-07-04 - 2006-07-04.