Skip to main content

Showing 1–11 of 11 results for author: Ramsay, S

Searching in archive cs. Search in all archives.
.
  1. arXiv:2409.14572  [pdf, other

    cs.CL cond-mat.mtrl-sci cs.AI cs.LG

    Evaluating the Performance and Robustness of LLMs in Materials Science Q&A and Property Predictions

    Authors: Hongchen Wang, Kangming Li, Scott Ramsay, Yao Fehlis, Edward Kim, Jason Hattrick-Simpers

    Abstract: Large Language Models (LLMs) have the potential to revolutionize scientific research, yet their robustness and reliability in domain-specific applications remain insufficiently explored. In this study, we evaluate the performance and robustness of LLMs for materials science, focusing on domain-specific question answering and materials property prediction across diverse real-world and adversarial c… ▽ More

    Submitted 11 March, 2025; v1 submitted 22 September, 2024; originally announced September 2024.

  2. arXiv:2307.06928  [pdf, ps, other

    cs.PL

    Ill-Typed Programs Don't Evaluate

    Authors: Steven Ramsay, Charlie Walpole

    Abstract: We introduce two-sided type systems, which are sequent calculi for typing formulas. Two-sided type systems allow for hypothetical reasoning over the typing of compound program expressions, and the refutation of typing formulas. By incorporating a type of all values, these type systems support more refined notions of well-typing and ill-typing, guaranteeing both that well-typed programs don't go wr… ▽ More

    Submitted 20 October, 2023; v1 submitted 13 July, 2023; originally announced July 2023.

    Comments: Incorporating anonymous reviewer suggestions from POPL'24

  3. Effect Handlers for Programmable Inference

    Authors: Minh Nguyen, Roly Perera, Meng Wang, Steven Ramsay

    Abstract: Inference algorithms for probabilistic programming are complex imperative programs with many moving parts. Efficient inference often requires customising an algorithm to a particular probabilistic model or problem, sometimes called inference programming. Most inference frameworks are implemented in languages that lack a disciplined approach to side effects, which can result in monolithic implement… ▽ More

    Submitted 23 December, 2024; v1 submitted 2 March, 2023; originally announced March 2023.

  4. arXiv:2210.14649  [pdf, ps, other

    cs.PL

    Higher-Order MSL Horn Constraints

    Authors: Jerome Jochems, Eddie Jones, Steven Ramsay

    Abstract: The monadic shallow linear (MSL) class is a decidable fragment of first-order Horn clauses that was discovered and rediscovered around the turn of the century, with applications in static analysis and verification. We propose a new class of higher-order Horn constraints which extend MSL to higher-order logic and develop a resolution-based decision procedure. Higher-order MSL Horn constraints can q… ▽ More

    Submitted 26 October, 2022; originally announced October 2022.

    Comments: Revision of conditionally accepted submission to POPL 2023

  5. arXiv:2111.12553  [pdf, other

    cs.PL

    CycleQ: An Efficient Basis for Cyclic Equational Reasoning

    Authors: Eddie Jones, C-. H. Luke Ong, Steven Ramsay

    Abstract: We propose a new cyclic proof system for automated, equational reasoning about the behaviour of pure functional programs. The key to the system is the way in which cyclic proof and equational reasoning are mediated by the use of contextual substitution as a cut rule. We show that our system, although simple, already subsumes several of the approaches to implicit induction variously known as "induc… ▽ More

    Submitted 14 June, 2022; v1 submitted 24 November, 2021; originally announced November 2021.

    Comments: Version accepted to PLDI'22

    ACM Class: F.3.1

  6. arXiv:2104.14175  [pdf, other

    cs.LO

    Initial Limit Datalog: a New Extensible Class of Decidable Constrained Horn Clauses

    Authors: Toby Cathcart Burn, Luke Ong, Steven Ramsay, Dominik Wagner

    Abstract: We present initial limit Datalog, a new extensible class of constrained Horn clauses for which the satisfiability problem is decidable. The class may be viewed as a generalisation to higher-order logic (with a simple restriction on types) of the first-order language limit Datalog$_Z$ (a fragment of Datalog modulo linear integer arithmetic), but can be instantiated with any suitable background theo… ▽ More

    Submitted 29 April, 2021; originally announced April 2021.

    Comments: 18 pages. To be published in LICS 2021

  7. arXiv:2012.13333  [pdf, ps, other

    cs.PL

    Verifying Liveness Properties of ML Programs

    Authors: M. M. Lester, R. P. Neatherway, C. -H. L. Ong, S. J. Ramsay

    Abstract: Higher-order recursion schemes are a higher-order analogue of Boolean Programs; they form a natural class of abstractions for functional programs. We present a new, efficient algorithm for checking CTL properties of the trees generated by higher-order recursion schemes, which is an extension of Kobayashi's intersection type-based model checking technique. We show that an implementation of this alg… ▽ More

    Submitted 24 December, 2020; originally announced December 2020.

    Comments: Peer-reviewed extended abstract presented at 2011 ACM SIGPLAN Workshop on ML. Full technical report archived at: https://ora.ox.ac.uk/objects/uuid:bf35bab8-b395-4f85-93bd-57ca0328a1d3

  8. Intensional Datatype Refinement

    Authors: Eddie Jones, Steven Ramsay

    Abstract: The pattern-match safety problem is to verify that a given functional program will never crash due to non-exhaustive patterns in its function definitions. We present a refinement type system that can be used to solve this problem. The system extends ML-style type systems with algebraic datatypes by a limited form of structural subtyping and environment-level intersection. We describe a fully autom… ▽ More

    Submitted 25 November, 2020; v1 submitted 4 August, 2020; originally announced August 2020.

    Comments: 26 pages plus bibliography and appendices. Tool available from https://github.com/bristolpl/intensional-datatys. [v2] fixed accidental unicode-related formatting issues in bibliography. [v3] Improvements incorporated, thanks to POPL 2021 reviewers

    ACM Class: F.3.1

  9. Bisimilarity in fresh-register automata

    Authors: Andrzej S. Murawski, Steven J. Ramsay, Nikos Tzevelekos

    Abstract: Register automata are a basic model of computation over infinite alphabets. Fresh-register automata extend register automata with the capability to generate fresh symbols in order to model computational scenarios involving name creation. This paper investigates the complexity of the bisimilarity problem for classes of register and fresh-register automata. We examine all main disciplines that have… ▽ More

    Submitted 5 February, 2025; v1 submitted 13 May, 2020; originally announced May 2020.

    Journal ref: Logical Methods in Computer Science, Volume 21, Issue 1 (February 6, 2025) lmcs:6476

  10. arXiv:1810.03598  [pdf, ps, other

    cs.PL

    Defunctionalization of Higher-Order Constrained Horn Clauses

    Authors: Long Pham, Steven J. Ramsay, C. -H. Luke Ong

    Abstract: Building on the successes of satisfiability modulo theories (SMT), Bjørner et al. initiated a research programme advocating Horn constraints as a suitable basis for automatic program verification. The notion of first-order constrained Horn clauses has recently been extended to higher-order logic by Cathcart Burn et al. To exploit the remarkable efficiency of SMT solving, a natural approach to solv… ▽ More

    Submitted 22 February, 2019; v1 submitted 8 October, 2018; originally announced October 2018.

    Comments: Some minor typos are fixed

    ACM Class: D.2.4; F.3.1; F.4.1

  11. arXiv:1705.06216  [pdf, ps, other

    cs.PL cs.LO

    Higher-Order Constrained Horn Clauses and Refinement Types

    Authors: Toby Cathcart Burn, C. -H. Luke Ong, Steven J. Ramsay

    Abstract: Motivated by applications in automated verification of higher-order functional programs, we develop a notion of constrained Horn clauses in higher-order logic and a decision problem concerning their satisfiability. We show that, although satisfiable systems of higher-order clauses do not generally have least models, there is a notion of canonical model obtained through a reduction to a problem con… ▽ More

    Submitted 1 August, 2017; v1 submitted 17 May, 2017; originally announced May 2017.

    Comments: Completely rewritten Section 4.3 on the correspondence between models to improve the clarity of the exposition. Various other minor improvements

    ACM Class: D.2.4; F.3.1; F.4.1