Programming Languages Papers
@ProgPapers
Followers
79
Following
1
Media
0
Statuses
2K
Programming languages: object-oriented programming, functional programming, logic programming. (new submissions to https://t.co/Fb8gxovwu3, not affiliated with arXiv)
Joined March 2010
Correct Black-Box Monitors for Distributed Deadlock Detection: Formalisation and Implementation (Technical Report).
arxiv.org
Many software applications rely on concurrent and distributed (micro)services that interact via message-passing and various forms of remote procedure calls (RPC). As these systems organically...
0
0
1
Place Capability Graphs: A General-Purpose Model of Rust's Ownership and Borrowing Guarantees.
arxiv.org
Rust's novel type system has proved an attractive target for verification and program analysis tools, due to the rich guarantees it provides for controlling aliasing and mutability. However, fully...
0
0
0
Complete the Cycle: Reachability Types with Expressive Cyclic References (Extended Version).
arxiv.org
Reachability Types (RT) are a qualified type system for tracking aliasing and separation in functional and higher-order programming. By formalizing resource reachability with a sound static type...
0
0
0
An LLM-powered Natural-to-Robotic Language Translation Framework with Correctness Guarantees.
arxiv.org
The Large Language Models (LLM) are increasingly being deployed in robotics to generate robot control programs for specific user tasks, enabling embodied intelligence. Existing methods primarily...
0
0
0
A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants.
arxiv.org
Large language models (LLMs) can potentially help with verification using proof assistants by automating proofs. However, it is unclear how effective LLMs are in this task. In this paper, we...
0
0
0
A2HCoder: An LLM-Driven Coding Agent for Hierarchical Algorithm-to-HDL Translation.
arxiv.org
In wireless communication systems, stringent requirements such as ultra-low latency and power consumption have significantly increased the demand for efficient algorithm-to-hardware deployment....
0
0
0
Linear Layouts: Robust Code Generation of Efficient Tensor Computation Using $\mathbb{F}_2$.
arxiv.org
Efficient tensor computation is a cornerstone of modern deep learning (DL) workloads, yet existing approaches struggle to achieve flexible and performant design and implementation of tensor...
0
0
0
Products of Recursive Programs for Hypersafety Verification (Extended Version).
arxiv.org
We study the problem of automated hypersafety verification of infinite-state recursive programs. We propose an infinite class of product programs, specifically designed with recursion in mind,...
0
0
1
Automated Discovery of Tactic Libraries for Interactive Theorem Proving.
arxiv.org
Enabling more concise and modular proofs is essential for advancing formal reasoning using interactive theorem provers (ITPs). Since many ITPs, such as Rocq and Lean, use tactic-style proofs,...
0
0
0
Efficient Decrease-and-Conquer Linearizability Monitoring.
arxiv.org
Linearizability has become the de facto correctness specification for implementations of concurrent data structures. While formally verifying such implementations remains challenging,...
0
0
1
To bind or not to bind? Discovering Stable Relationships in Object-centric Processes (Extended Version).
arxiv.org
Object-centric process mining investigates the intertwined behavior of multiple objects in business processes. From object-centric event logs, object-centric Petri nets (OCPN) can be discovered to...
0
0
0
Compositional Verification in Concurrent Separation Logic with Permissions Regions.
arxiv.org
Concurrent separation logic with fractional permissions (CSLPerm) provides a promising reasoning system to verify most complex sequential and concurrent fine-grained programs. The logic with...
0
0
1
Who Wins the Race? (R Vs Python) - An Exploratory Study on Energy Consumption of Machine Learning Algorithms.
arxiv.org
The utilization of Machine Learning (ML) in contemporary software systems is extensive and continually expanding. However, its usage is energy-intensive, contributing to increased carbon emissions...
0
0
0
Syntactic Completions with Material Obligations.
arxiv.org
Code editors provide essential services that help developers understand, navigate, and modify programs. However, these services often fail in the presence of syntax errors. Existing syntax error...
0
1
0
SafeTree: Expressive Tree Policies for Microservices.
arxiv.org
A microservice-based application is composed of multiple self-contained components called microservices, and controlling inter-service communication is important for enforcing safety properties....
0
1
0
Software Model Checking via Summary-Guided Search (Extended Version).
arxiv.org
In this work, we describe a new software model-checking algorithm called GPS. GPS treats the task of model checking a program as a directed search of the program states, guided by a compositional,...
0
0
1
ARSP: Automated Repair of Verilog Designs via Semantic Partitioning.
arxiv.org
Debugging functional Verilog bugs consumes a significant portion of front-end design time. While Large Language Models (LLMs) have demonstrated great potential in mitigating this effort, existing...
0
0
0
Leveraging Large Language Models to Detect Missed Peephole Optimizations.
arxiv.org
By replacing small, suboptimal instruction sequences within programs with a more efficient equivalent, peephole optimization can not only directly optimize code size and performance, but also...
0
0
0