编程语言
Domain-specific languages for hardware can significantly enhance designer productivity, but sometimes at the cost of ease of verification. On the other hand, ISA specification languages are too static to be used during early stage design…
The graphical modeling language GRAFCET is used as a formal specification language in industrial control design. This paper proposes a static analysis approach based on the control flow of GRAFCET using abstract interpretation to allow…
Many data extraction tasks of practical relevance require not only syntactic pattern matching but also semantic reasoning about the content of the underlying text. While regular expressions are very well suited for tasks that require only…
Several relational program logics have been introduced for integrating reasoning about relational properties of programs and measurement of quantitative difference between computational effects. Towards a general framework for such logics,…
Tydi is an open specification for streaming dataflow designs in digital circuits, allowing designers to express how composite and variable-length data structures are transferred over streams using clear, data-centric types. This provides a…
We present a small-step, frame stack style, semantics for sequential Core Erlang, a dynamically typed, impure functional programming language. The semantics and the properties that we prove are machine-checked with the Coq proof assistant.…
Common data types like dates, addresses, phone numbers and tables can have multiple textual representations, and many heavily-used languages, such as SQL, come in several dialects. These variations can cause data to be misinterpreted,…
Tau Prolog is a client-side Prolog interpreter fully implemented in JavaScript, which aims at implementing the ISO Prolog Standard. Tau Prolog has been developed to be used with either Node.js or a browser seamlessly, and therefore, it has…
Concurrency theory has received considerable attention, but mostly in the scope of synchronous process algebras such as CCS, CSP, and ACP. As another way of handling concurrency, data-based coordination languages aim to provide a clear…
When a new programming language appears, the syntax and intended behaviour of its programs need to be specified. The behaviour of each language construct can be concisely specified by translating it to fundamental constructs (funcons),…
Memory-safety issues and information leakage are known to be depressingly common. We consider the compositional static detection of these kinds of vulnerabilities in first-order C-like programs. Indeed the latter are relational hyper-safety…
Amortized analysis is a program cost analysis technique for data structures in which the cost of operations is specified in aggregate, under the assumption of continued sequential use. Typically, amortized analyses are presented…
We present a logically principled foundation for systematizing, in a way that works with any computational effect and evaluation order, SMT constraint generation seen in refinement type systems for functional programming languages. By…
High-level synthesis (HLS) is a process that automatically translates a software program in a high-level language into a low-level hardware description. However, the hardware designs produced by HLS tools still suffer from a significant…
Disco is a pure, strict, statically typed functional programming language designed to be used in the setting of a discrete mathematics course. The goals of the language are to introduce students to functional programming concepts early, and…
Regular expressions in an Automata Theory and Formal Languages course are mostly treated as a theoretical topic. That is, to some degree their mathematical properties and their role to describe languages is discussed. This approach fails to…
This paper describes a way to improve the scalability of program synthesis by exploiting modularity: larger programs are synthesized from smaller programs. The key issue is to make each "larger-created-from-smaller" synthesis sub-problem be…
In this article, we introduce an instruction set architecture (ISA) for processing-in-memory (PIM) based deep neural network (DNN) accelerators. The proposed ISA is for DNN inference on PIM-based architectures. It is assumed that the…
DSLs and hardware accelerators have proven to be very effective in optimizing computationally expensive workloads. In this paper, we propose a solution to the challenge of manually rewriting legacy or unoptimized code in domain-specific…
Multi-Level Intermediate Representation (MLIR) is a novel compiler infrastructure that aims to provide modular and extensible components to facilitate building domain specific compilers. However, since MLIR models programs at an…