default search action
Robert Atkey
Person information
- affiliation: University of Strathclyde, Department of Computer and Information Sciences, Glasgow, UK
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
- [j10]Robert Atkey
:
Polynomial Time and Dependent Types. Proc. ACM Program. Lang. 8(POPL): 2288-2317 (2024) - [i8]Matthew L. Daggitt, Wen Kokke, Robert Atkey, Natalia Slusarz, Luca Arnaboldi, Ekaterina Komendantskaya:
Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs. CoRR abs/2401.06379 (2024) - [i7]Matthew L. Daggitt, Wen Kokke, Robert Atkey:
Efficient compilation of expressive problem space specifications to neural network solvers. CoRR abs/2402.01353 (2024) - [i6]Robert Atkey, Wen Kokke:
A Semantic Proof of Generalised Cut Elimination for Deep Inference. CoRR abs/2404.06233 (2024) - 2023
- [c29]Matthew L. Daggitt, Wen Kokke, Ekaterina Komendantskaya, Robert Atkey, Luca Arnaboldi, Natalia Slusarz, Marco Casadio, Ben Coke, Jeonghyeon Lee:
The Vehicle Tutorial: Neural Network Verification with Vehicle. FoMLAS@CAV 2023: 1-5 - [c28]Matthew L. Daggitt
Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively. CPP 2023: 102-120 - [i5]Robert Atkey:
Polynomial Time and Dependent Types. CoRR abs/2307.09145 (2023) - 2022
- [c27]James Wood
A Framework for Substructural Type Systems. ESOP 2022: 376-402 - [i4]Matthew L. Daggitt, Wen Kokke, Robert Atkey, Luca Arnaboldi, Ekaterina Komendantskaya:
Vehicle: Interfacing Neural Network Verifiers with Interactive Theorem Provers. CoRR abs/2202.05207 (2022) - 2021
- [j9]Guillaume Allais
A type- and scope-safe universe of syntaxes with binding: their semantics and proofs. J. Funct. Program. 31: e22 (2021) - 2020
- [j8]Daniel Hillerström
Effect handlers via generalised continuations. J. Funct. Program. 30: e5 (2020) - [c26]Wen Kokke, Ekaterina Komendantskaya, Daniel Kienitz, Robert Atkey, David Aspinall:
Neural Networks, Secure by Construction - An Exploration of Refinement Types. APLAS 2020: 67-85 - [c25]James Wood, Robert Atkey:
A Linear Algebra Approach to Linear Metatheory. Linearity&TLLA@IJCAR-FSCD 2020: 195-212 - [c24]Robert Atkey, Bruno Gavranovic, Neil Ghani, Clemens Kupke
Compositional Game Theory, Compositionally. ACT 2020: 198-214 - [i3]Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, James McKinna:
A Type and Scope Safe Universe of Syntaxes with Binding: Their Semantics and Proofs. CoRR abs/2001.11001 (2020)
2010 – 2019
- 2019
- [j7]Kenji Maillard
Dijkstra monads for all. Proc. ACM Program. Lang. 3(ICFP): 104:1-104:29 (2019) - [i2]Kenji Maillard, Danel Ahman, Robert Atkey, Guido Martínez, Catalin Hritcu, Exequiel Rivas, Éric Tanter:
Dijkstra Monads for All. CoRR abs/1903.01237 (2019) - 2018
- [j6]Guillaume Allais
A type and scope safe universe of syntaxes with binding: their semantics and proofs. Proc. ACM Program. Lang. 2(ICFP): 90:1-90:30 (2018) - [c23]Robert Atkey:
Syntax and Semantics of Quantitative Type Theory. LICS 2018: 56-65 - [e2]Robert Atkey, Sam Lindley:
Proceedings of the 7th Workshop on Mathematically Structured Functional Programming, MSFP@FSCD 2018, Oxford, UK, 8th July 2018. EPTCS 275, 2018 [contents] - 2017
- [c22]Robert Atkey:
Observed Communication Semantics for Classical Processes. ESOP 2017: 56-82 - [c21]Daniel Hillerström
Continuation Passing Style for Effect Handlers. FSCD 2017: 18:1-18:19 - [i1]Robert Atkey, Michel Steuwer
Strategy Preserving Compilation for Parallel Functional Code. CoRR abs/1710.08332 (2017) - 2016
- [c20]Robert Atkey
Conflation Confers Concurrency. A List of Successes That Can Change the World 2016: 32-55 - [e1]Robert Atkey, Neelakantan R. Krishnaswami:
Proceedings 6th Workshop on Mathematically Structured Functional Programming, MSFP@ETAPS 2016, Eindhoven, Netherlands, 8th April 2016. EPTCS 207, 2016 [contents] - 2015
- [j5]Robert Atkey, Donald Sannella:
ThreadSafe: Static Analysis for Java Concurrency. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 72 (2015) - [j4]Robert Atkey
Interleaving data and effects. J. Funct. Program. 25 (2015) - [c19]Robert Atkey, Neil Ghani, Fredrik Nordvall Forsberg
Models for Polymorphism over Physical Dimension. TLCA 2015: 45-59 - 2014
- [c18]Robert Atkey
From parametricity to conservation laws, via Noether's theorem. POPL 2014: 491-502 - [c17]Robert Atkey
A relationally parametric model of dependent type theory. POPL 2014: 503-516 - 2013
- [c16]Robert Atkey, Conor McBride:
Productive coprogramming with guarded recursion. ICFP 2013: 197-208 - [c15]Robert Atkey
Abstraction and invariance for algebraically indexed types. POPL 2013: 87-100 - 2012
- [j3]Robert Atkey
Refining Inductive Types. Log. Methods Comput. Sci. 8(2) (2012) - [c14]Robert Atkey:
Relational Parametricity for Higher Kinds. CSL 2012: 46-61 - [c13]Robert Atkey
Fibrational Induction Meets Effects. FoSSaCS 2012: 42-57 - [c12]Robert Atkey:
The Semantics of Parsing with Semantic Actions. LICS 2012: 75-84 - 2011
- [j2]Robert Atkey
Amortised Resource Analysis with Separation Logic. Log. Methods Comput. Sci. 7(2) (2011) - [c11]Robert Atkey
When Is a Type Refinement an Inductive Type? FoSSaCS 2011: 72-87 - 2010
- [c10]Ewen Maclean, Andrew Ireland, Lucas Dixon, Robert Atkey:
Refinement and Term Synthesis in Loop Invariant Generation. WING@ETAPS/IJCAR 2010: 167-182 - [c9]Robert Atkey
Amortised Resource Analysis with Separation Logic. ESOP 2010: 85-103 - [c8]David Aspinall, Robert Atkey
Symbolic and Analytic Techniques for Resource Analysis of Java Bytecode. TGC 2010: 1-22
2000 – 2009
- 2009
- [j1]Robert Atkey
Parameterised notions of computation. J. Funct. Program. 19(3-4): 335-376 (2009) - [c7]Robert Atkey
Algebras for Parameterised Monads. CALCO 2009: 3-17 - [c6]Robert Atkey
Unembedding domain-specific languages. Haskell 2009: 37-48 - [c5]Robert Atkey
Syntax for Free: Representing Syntax with Binding Using Parametricity. TLCA 2009: 35-49 - 2008
- [c4]Robert Atkey:
What is a Categorical Model of Arrows? MSFP@ICALP 2008: 19-37 - 2007
- [c3]Robert Atkey:
CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types. TYPES 2007: 18-32 - 2006
- [c2]Robert Atkey:
Parameterised Notions of Computation. MSFP@MPC 2006 - 2004
- [c1]Robert Atkey:
A lambda-Calculus for Resource Separation. ICALP 2004: 158-170
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-05-31 01:40 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: