Robert Atkey

Proc. ACM Program. Lang., January, 2024

A Semantic Proof of Generalised Cut Elimination for Deep Inference.

[BibT_eX]

[DOI]

CoRR, 2024

Efficient compilation of expressive problem space specifications to neural network solvers.

[BibT_eX]

[DOI]

Matthew L. Daggitt

CoRR, 2024

Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs.

[BibT_eX]

[DOI]

CoRR, 2024

2023

Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively.

[BibT_eX]

[DOI]

Matthew L. Daggitt

Luca Arnaboldi

Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2023

The Vehicle Tutorial: Neural Network Verification with Vehicle.

[BibT_eX]

[DOI]

Matthew L. Daggitt

Proceedings of the 6th Workshop on Formal Methods for ML-Enabled Autonomous Systems, 2023

2022

Vehicle: Interfacing Neural Network Verifiers with Interactive Theorem Provers.

[BibT_eX]

[DOI]

CoRR, 2022

A Framework for Substructural Type Systems.

[BibT_eX]

[DOI]

James Wood

Proceedings of the Programming Languages and Systems, 2022

2020

Effect handlers via generalised continuations.

[BibT_eX]

[DOI]

Daniel Hillerström

Fredrik Nordvall Forsberg

J. Funct. Program., 2020

Compositional Game Theory, Compositionally.

[BibT_eX]

[DOI]

Proceedings of the 3rd Annual International Applied Category Theory Conference 2020, 2020

A Linear Algebra Approach to Linear Metatheory.

[BibT_eX]

[DOI]

James Wood

Proceedings of the Proceedings Second Joint International Workshop on Linearity & Trends in Linear Logic and Applications, 2020

Neural Networks, Secure by Construction - An Exploration of Refinement Types.

[BibT_eX]

[DOI]

Daniel Kienitz

David Aspinall

Proceedings of the Programming Languages and Systems - 18th Asian Symposium, 2020

2019

Dijkstra monads for all.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2019

2018

A type and scope safe universe of syntaxes with binding: their semantics and proofs.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2018

Syntax and Semantics of Quantitative Type Theory.

[BibT_eX]

[DOI]

Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018

2017

Strategy Preserving Compilation for Parallel Functional Code.

[BibT_eX]

[DOI]

CoRR, 2017

Continuation Passing Style for Effect Handlers.

[BibT_eX]

[DOI]

Daniel Hillerström

K. C. Sivaramakrishnan

Proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction, 2017

Observed Communication Semantics for Classical Processes.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2017

2016

Conflation Confers Concurrency.

[BibT_eX]

[DOI]

J. Garrett Morris

Proceedings of the A List of Successes That Can Change the World, 2016

2015

Interleaving data and effects.

[BibT_eX]

[DOI]

J. Funct. Program., 2015

ThreadSafe: Static Analysis for Java Concurrency.

[BibT_eX]

[DOI]

Donald Sannella

Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2015

Models for Polymorphism over Physical Dimension.

[BibT_eX]

[DOI]

Fredrik Nordvall Forsberg

Timothy Revell

Sam Staton

Proceedings of the 13th International Conference on Typed Lambda Calculi and Applications, 2015

2014

A relationally parametric model of dependent type theory.

[BibT_eX]

[DOI]

Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

From parametricity to conservation laws, via Noether's theorem.

[BibT_eX]

[DOI]

Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

2013

Abstraction and invariance for algebraically indexed types.

[BibT_eX]

[DOI]

Andrew Kennedy

Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2013

Productive coprogramming with guarded recursion.

[BibT_eX]

[DOI]

Conor McBride

Proceedings of the ACM SIGPLAN International Conference on Functional Programming, 2013

2012

Refining Inductive Types

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2012

The Semantics of Parsing with Semantic Actions.

[BibT_eX]

[DOI]

Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, 2012

Fibrational Induction Meets Effects.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computational Structures, 2012

Relational Parametricity for Higher Kinds.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic (CSL'12), 2012

2011

Amortised Resource Analysis with Separation Logic

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2011

When Is a Type Refinement an Inductive Type?

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computational Structures, 2011

2010

Symbolic and Analytic Techniques for Resource Analysis of Java Bytecode.

[BibT_eX]

[DOI]

Proceedings of the Trustworthly Global Computing - 5th International Symposium, 2010

Refinement and Term Synthesis in Loop Invariant Generation.

[BibT_eX]

[DOI]

Proceedings of the Second International Workshop on Invariant Generation, 2010

2009

Parameterised notions of computation.

[BibT_eX]

[DOI]

J. Funct. Program., 2009

Syntax for Free: Representing Syntax with Binding Using Parametricity.

[BibT_eX]

[DOI]

Proceedings of the Typed Lambda Calculi and Applications, 9th International Conference, 2009

Unembedding domain-specific languages.

[BibT_eX]

[DOI]

Jeremy Yallop

Proceedings of the 2nd ACM SIGPLAN Symposium on Haskell, 2009

Algebras for Parameterised Monads.

[BibT_eX]

[DOI]

Proceedings of the Algebra and Coalgebra in Computer Science, 2009

2008

What is a Categorical Model of Arrows?

[BibT_eX]

[DOI]

Proceedings of the Second Workshop on Mathematically Structured Functional Programming, 2008

2007

CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types.

[BibT_eX]

[DOI]

Proceedings of the Types for Proofs and Programs, International Conference, 2007

2004

A lambda-Calculus for Resource Separation.

[BibT_eX]

[DOI]