Programming Languages

New submissions

• New submissions
• Cross-lists
• Replacements

New submissions for Fri, 20 May 22

[1]  arXiv:2205.09246 [pdf, ps, other]

Title: Transformer-based Program Synthesis for Low-Data Environments

Authors: Jack Roper

Comments: 11 pages. Corpus can be found at this https URL

Subjects: Programming Languages (cs.PL); Machine Learning (cs.LG)

Recent advancements in large pre-trained transformer models (GPT2/3, T5) have found use in program synthesis to generate programs that satisfy a set of input/output examples. However, these models perform poorly on long-horizon and low-data tasks, and often don't seem to understand the semantics of the languages they generate. We investigate an approach that tackles both of these issues, by using attributed context-free-grammars of programming languages to generate programs, and then analyzing generated programs so that they can be annotated with compile and runtime attributes, such as types, so that information about the program can be remembered during long-horizon generation. We firstly find that synthesized datasets can be made efficiently and can provide transformer models with enough data in order to perform well on some synthesis tasks. We also find that giving models access to program attributes is especially effective in low-data environments, and tends improve the quality and reduce errors of transformer-generated programs.

[2]  arXiv:2205.09655 [pdf, other]

Title: Primrose: Selecting Container Data Types by their Properties

Authors: Xueying Qin, Liam O'Connor, Michel Steuwer

Subjects: Programming Languages (cs.PL); Data Structures and Algorithms (cs.DS)

Container data types are ubiquitous in computer programming, enabling developers to efficiently store and process collections of data with an easy-to-use programming interface. Many programming languages offer a variety of container implementations in their standard libraries based on data structures offering different capabilities and performance characteristics. Choosing the best container for an application is not straightforward, as performance characteristics can change drastically in different scenarios, and real-world performance is not always correlated to theoretical complexity. In this paper, we present Primrose, a language-agnostic tool for selecting the best performing valid container implementation from a set of container data types that satisfy the given properties. Semantic properties allow application developers to specify the expected behaviour of a container as a type refinement, e.g., if the container should only contain unique values (such as a set) or should satisfy the LIFO property of a stack. Semantic properties nicely complement syntactic properties (i.e., traits, interfaces, or type classes), allowing developers to specify a container's programming interface and behaviour without committing to a concrete implementation. Primrose automatically select the set of valid container implementations for which the library specifications, written by the developers of container libraries, satisfies the specified properties. Finally, Primrose ranks the valid library implementations based on their runtime performance. We present our prototype implementation of Primrose that preprocesses annotated Rust code, selecting the best performing container implementation. Primrose is easy to integrate in other programming languages. We encode properties and library specifications into verification conditions in a SMT solver to determine the set of valid container implementations.

Cross-lists for Fri, 20 May 22

[3]  arXiv:2205.09556 (cross-list from cs.LO) [pdf, ps, other]

Title: Neural Networks in Imandra: Matrix Representation as a Verification Choice

Authors: Remi Desmartin, Grant Passmore, Ekaterina Komendantskaya

Comments: Submitted as informal talk to FOMLAS'22

Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL)

The demand for formal verification tools for neural networks has increased as neural networks have been deployed in a growing number of safety-critical applications. Matrices are a data structure essential to formalising neural networks. Functional programming languages encourage diverse approaches to matrix definitions. This feature has already been successfully exploited in different applications. The question we ask is whether, and how, these ideas can be applied in neural network verification. A functional programming language Imandra combines the syntax of a functional programming language and the power of an automated theorem prover. Using these two key features of Imandra, we explore how different implementations of matrices can influence automation of neural network verification.

Replacements for Fri, 20 May 22

[4]  arXiv:2205.07979 (replaced) [pdf, ps, other]

Title: The Budge programming language

Authors: Boro Sitnikovski

Subjects: Programming Languages (cs.PL); Computation and Language (cs.CL); Logic in Computer Science (cs.LO)

[5]  arXiv:2205.08768 (replaced) [pdf, other]

Title: Global Type Inference for Featherweight Generic Java

Authors: Andreas Stadelmeier, Martin Plümicke, Peter Thiemann

Comments: 33 pages, abridged version appears in ECOOP 2022

Subjects: Programming Languages (cs.PL)

[6]  arXiv:2205.05781 (replaced) [pdf, ps, other]

Title: VyZX : A Vision for Verifying the ZX Calculus

Authors: Adrian Lehmann, Ben Caldwell, Robert Rand

Comments: 12 pages

Subjects: Quantum Physics (quant-ph); Programming Languages (cs.PL)

• New submissions
• Cross-lists
• Replacements