title: SureDistrib: Verifying Almost-Sure Termination of Composite Asynchronous Byzantine Protocols

authors:
Longfei Qiu
Jingqi Xiao
Ji-Yong Shin
Zhong Shao

abstract: Consensus algorithms play a central role in many distributed systems, including blockchains. The most practical consensus algorithms are based on the partial synchrony model. While partially synchronous protocols are relatively simple, they cannot maintain liveness when the message delivery latency is uncertain. Asynchronous protocols do not rely on bounded latency to maintain liveness, but they are much more difficult to understand and implement, being usually described as a composition of several layers of algorithms. Moreover, due to the FLP impossibility theorem, they only provide probabilistic liveness guarantees. These factors make the correctness of asynchronous protocols challenging to verify, and there have been liveness bugs in these protocols that remain unnoticed for years. We introduce SureDistrib, a formal framework for specifying and verifying probabilistic safety and liveness properties of asynchronous distributed protocols. Our framework supports specifying probabilistic algorithms that depend on other probabilistic functionalities, such as binary agreement algorithms depending on common coins. We define refinement relations for such systems, and prove composition lemmas that replace the underlay functionality with an implementation, so that the composed system refines the original system with an abstract underlay. Based on our framework, we give the first mechanized proof that an asynchronous byzantine fault-tolerant binary agreement algorithm terminates with probability 1 (“almost-sure termination”).


venue: pldi

title: Flow-Analysis-Based Closure Optimization

authors:
John H. Reppy
Olin Shivers
Byron Zhong

abstract: One of the key implementation challenges for higher-order functional languages is managing the representation of first-class function values. The standard approach to this problem is closure conversion, which is a compiler transformation that introduces an explicit data structure to represent the environment of a function value. Constructing the closure for a nested function usually involves copying data from the enclosing function’s closure. To avoid this copying, one might use linked representations, but that choice makes variable access slow and can introduce space leaks. Shao and Appel developed an effective closure converter that reduces copying and is safe-for-space, but their converter is based on a weak, first-order analysis. In this paper, we present a new safe-for-space closure converter that uses a higher-order flow analysis to inform closure-representation decisions. We describe how this information can be used to improve two aspects of closure optimization: sharing heap-allocated tuples of variables and spreading variables into argument registers. We have implemented our converter in the Standard ML of New Jersey system and demonstrated that it produces better code on average than the Shao and Appel converter, with significant performance gains for some benchmarks.


title: Bonsai: Compiling Queries to Pruned Tree Traversals

authors:
Alexander J. Root
Christophe Gyurgyik
Purvi Goel
Kayvon Fatahalian
Jonathan Ragan-Kelley
Andrew Adams
Fredrik Kjolstad

abstract: Trees can accelerate queries that search or aggregate values over large collections. They achieve this by storing metadata that enables quick pruning (or inclusion) of subtrees when predicates on that metadata can prove that none (or all) of the data in a subtree affect the query result. Existing systems implement this pruning logic manually for each query predicate and data structure. We generalize and mechanize this class of optimization. Our method derives conditions for when subtrees can be pruned (or included wholesale), expressed in terms of the metadata available at each node. We efficiently generate these conditions using symbolic interval analysis, extended with new rules to handle geometric predicates (e.g., intersection, containment). Additionally, our compiler fuses compound queries (e.g., reductions on filters) into a single tree traversal. These techniques enable the automatic derivation of generalized single-index and dual-index tree joins that support a wide class of join predicates beyond standard equality and range predicates. The generated traversals match the behavior of expert-written code that implements query-specific traversals, and can asymptotically outperform the linear scans and nested-loop joins that existing systems fall back to when hand-written cases do not apply.


title: Cerisier: A Program Logic for Attestation in a Capability Machine

authors:
June Rousseau
Denis Carnier
Thomas Van Strydonck
Steven Keuchel
Dominique Devriese
Lars Birkedal

abstract: A key feature in trusted computing is attestation, which allows encapsulated components (enclaves) to prove their identity to (local or remote) distrusting components. Reasoning about software that uses the technique requires tracking how trust evolves after successful attestation. This process is security-critical and non-trivial, but no existing formal verification technique supports modular reasoning about attestation of enclaves and their clients, or proving end-to-end properties for systems combining trusted, untrusted and attested code. We contribute Cerisier, the first program logic for modular reasoning about trusted, untrusted and attested code, fully mechanized in the Iris separation logic and the Rocq Prover. We formalize a recent proposal, CHERI-TrEE, to extend capability machines with enclave primitives, as an extension to the Cerise capability machine and program logic. Our program logic comes with a universal contract for untrusted code, which captures both capability safety and local enclave attestation. Like Cerise, this universal contract is phrased in terms of a logical relation defining capabilities’ authority. We demonstrate Cerisier by proving end-to-end properties for three representative applications of trusted computing: secure outsourced computation, mutual attestation and a modeled trusted sensor component.


title: CoTenN: Constrained Optimization with Tensor Networks

authors:
Ritvik Sharma
Cheng Peng
Siddharth Dangwal
Sara Achour

abstract: Simulation of physics problems is one of the most important use cases of quantum computing. For this class of problems, the goal is typically to find the minimum energy state, or the ground state, of a physical system’s Hamiltonian. These problems frequently have constraints, such as symmetry conditions, which must also be satisfied. To solve such problems, researchers in computational physics use quantum-inspired algorithms that execute on classical computers. In particular, tensor network-based eigensolvers such as DMRG have become popular. However, to use these eigensolvers, the constrained optimization problem must first be encoded as a tensor network that implements a low-rank decomposition of the system’s Hamiltonian and state vector. These tensor network encodings are highly flexible, allowing for variables with ≥2 quantum states and supporting efficient constraint encodings that directly constrain the state vector. A critical challenge to developing tensor networkbased encodings is that, currently, the encoding process is manual; significant effort is required to identify an efficient encoding for a new physics problem. In this work, we introduce a quantum constrained optimization problem (QCOP), a general abstraction for describing minimization problems over quantum variables that are subject to hard constraints. We present Masq , the first constraint programming language for QCOPs implementable with tensor networks, and CoTenN , a compiler that automatically maps QCOPs specified with Masq programs to tensor networks. To demonstrate the utility of Masq and CoTenN , we formulate two physics problems in Masq and then use CoTenN to find their ground states. We find the CoTenN -generated tensor networks generally outperform SOTA problem formulations, providing between 2.05 × − 53.32 × total speedups across runs for QCOPs and yielding up to 2.49 ⋅ 10 7 × lower truncation errors for otherwise unconstrained problems.


title: Abstract Interpretation with Confidence: Quantifying the Precision of Dataflow Analysis with Probabilities

authors:
Yuanfeng Shi
Ziyue Jin
Xin Zhang

abstract: Abstract interpretation has served as a foundational framework for static program analysis, enabling the over approximation of program semantics to be sound (i.e., no false negatives) but often at the cost of false alarms due to incompleteness. Although prior efforts to address false alarms have incorporated probabilistic techniques to compute confidence values for alarms, these methods are largely guided by empirical intuitions and lack a theoretical foundation. This paper bridges this gap by proposing a principled framework to quantify the confidence in results produced by a dataflow analysis based on abstract interpretation. Specifically, we define the problem as calculating the probability of the abstract interpreter being locally complete for a sampled program from the distribution of programs consistent with such abstract interpretation. By proposing a compositional denotational semantics ⟨ ⟨ ⋅ ⟩ ⟩ , we derive the distribution of program outputs to compute those confidence probabilities. Moreover, to ensure tractability, we propose another denotational semantics ⟨ ⟨ ⋅ ⟩ ⟩ l c that under-approximates ⟨ ⟨ ⋅ ⟩ ⟩ . The paper proves both the correctness of the two semantics, and therefore establishes a theoretical foundation for quantifying the precision of static program analysis with probabilities.


title: Fungible Memories for Automated Technology Mapping and Retargeting

authors:
Zachary D. Sisco
Sijie Kong
Daniel Ruelas-Petrisko
Jingtao Xia
Julian Springer
Varun Rao
Spencer Wang
Gus Henry Smith
Ben Hardekopf
Jonathan Balkind

abstract: During chip development, engineers must target different technologies, such as simulation and various ASIC and FPGA technologies. Conventionally, they split parts of the code (e.g., memories) into separate technology-specialized blocks implementing the same high-level behavior. This leads to brittle code, with multiple but subtly different blocks describing the same semantic behavior, harming verification, agility, and extensibility. We propose fungible memories , an HDL-level “write once, map anywhere” memory abstraction with rich enough semantics to automatically target all relevant technologies using a single generic interface. We incorporate fungible memories into a compiler called Memo . For designs without a specific technology mapping, we also present a memory decompiler which lifts memories from an existing gate-level design to Memo , enabling automated technology retargeting, which is a holy grail for digital designers. We present a structure-aware equality saturation technique which scales to netlists with millions of cells and identifies memories that the state of the art cannot. We demonstrate that Memo effectively targets backends across different technology platforms (simulation, ASIC, and FPGA) over a suite of representative designs, including a RISC-V multicore SoC.


title: Enumerating Ill-Typed Programs for Testing Type Analyzers

authors:
Thodoris Sotiropoulos
Zhendong Su

abstract: We propose error enumeration , a method that aims to discover soundness defects in type analyzers by generating ill-typed programs by construction. Given a well-typed program 𝑃 , it systematically injects type mismatches at all possible program locations to explore ill-typed programs that differ from 𝑃 by replacing one expression with incompatible ones. The core contributions of our work are: (1) soundly injecting type mismatches even in the presence of type inference and refinements, and (2) enabling practical exploration of large seed programs by pruning the search space. Incomplete type information complicates the injection of type mismatches, as type inference can silently "repair" the injected error by adjusting inferred types in the surrounding context so that the program still type-checks. We address this by introducing a lightweight, usage-based reasoning technique that recovers missing types of program elements by leveraging the existing type annotations at each element’s use site. This enables the injection of errors that guarantee type incompatibilities at the use sites of variables and other expressions. Finally, to prune the search space, we enumerate only those errors that ultimately lead to comparisons between types with distinct shape characteristics. We evaluated our implementation, Eris , on (1) three type analyzers integrated into the compilers of Kotlin, Scala, and Groovy, and (2) the Checker Framework, widely used to identify null-related errors in Java programs. Eris has uncovered 64 bugs caused by ill-typed programs: 51 leading to unsoundness, and 13 to compiletime crashes. Further investigation reveals that the majority of the soundness bugs discovered by Eris are triggered under highly complex conditions, where error injection requires (1) specific combinations of actual vs. expected type pairs at deeply-nested program locations, or (2) reasoning about control flow and missing type information, capabilities that lie beyond the scope of existing work.


title: Editorial Message

abstract: The Proceedings of the ACM series presents the highest-quality research conducted in diverse areas of computer science, as represented by the ACM Special Interest Groups (SIGs). The Proceedings of the ACM on Programming Languages (PACMPL) focuses on research on all aspects of programming languages, from design to implementation and from mathematical formalisms to empirical studies. The journal operates in close collaboration with the ACM Special Interest Group on Programming Languages (SIGPLAN) and is committed to making high-quality peer-reviewed scientific research in programming languages free of restrictions on both access and use.


title: SuperCollider: Scalable and Effective Data Race Detection for CUDA

authors:
Mark Stephenson
Sana Damani
Mohamed Tarek Ibn Ziad
Anis Ladram
Michael Garland

abstract: Data races, which occur when two or more threads incorrectly access the same memory location without appropriate synchronization, cause CUDA programmers considerable pain. Even experts struggle to reason about extreme parallelism, multiple memory spaces and scopes, and diverse synchronization mechanisms. Races can manifest as subtle data corruption, deadlock, or livelock, which are difficult to reproduce in a debugging environment. To date, there is no generally reliable tool for identifying races in GPU programs at scale. State-of-the-art dynamic GPU race detectors attempt to detect data races by faithfully tracking the memory operations, barriers, and memory fences executed by tens of thousands of threads. While this complexity enables the detection of subtle races, it comes with a cost: existing tools incur substantial memoryfootprint overheads (e.g., greater than 9×) and/or runtime overheads (e.g., 1000×), and tend to report false positives. This paper introduces SuperCollider, a simple race detector for CUDA that tracks only threadlevel state, is agnostic to synchronization protocols, introduces no memory-footprint overhead, seamlessly handles shared, global, and tensor memory spaces, does not produce false positives, and is relatively fast. Although SuperCollider cannot detect all races, we demonstrate that it effectively catches many data races in professionally authored CUDA programs, including races that prior art cannot. Our approach exposed over 90 data races across libraries and CUDA benchmarks, and even found a race in the CUDA Programming Guide. Unlike prior art, SuperCollider can operate at the extreme scales required by modern GPU workloads.


title: Dynamically Checked Deep Immutability in Python

authors:
Fridtjof Peer Stoldt
Sylvan Clebsch
Matthew A. Johnson
Matthew J. Parkinson
Tobias Wrigstad

abstract: Immutability is common in the programming mainstream: deep immutability is the default in functional languages while imperative languages typically provide opt-in support for shallow immutability, usually enforced through static checking. Python is a dynamic imperative language where mutability is inherent: not only are most objects mutable, but programs themselves—modules, classes, functions—are represented by mutable objects at run-time, and libraries routinely rely on this mutability. This makes adding immutability to Python a significant challenge. This paper presents the design and implementation of deep immutability for Python. Our primary motivation is to permit multiple sub-interpreters to directly share object references, which currently requires costly serialisation. Sharing via immutability introduces a soundness challenge, as a violation could corrupt the interpreter’s state. We identify numerous challenges that stem from decades of design decisions that did not anticipate immutability, and show how they can be overcome through two complementary techniques: detachment , which severs run-time links that would cause immutability to propagate too widely, and freezability , which gives objects run-time control over whether and how they may become immutable. Together, these principles form a general design pattern for deep immutability in dynamic languages. We validate our design with an implementation on CPython 3.15 that is backwards-compatible with existing programs and enables direct, zero-copy sharing of immutable objects across sub-interpreters.


title: Heterogeneous Dynamic Logic: Provability Modulo Program Theories

authors:
Samuel Teuber
Mattias Ulbrich
André Platzer
Bernhard Beckert

abstract: Formally specifying, let alone verifying, properties of systems involving multiple programming languages is inherently challenging. We introduce Heterogeneous Dynamic Logic (HDL), a framework for combining reasoning principles from distinct (dynamic) program logics in a modular and compositional way. HDL mirrors the architecture of satisfiability modulo theories (SMT): Individual dynamic logics, along with their calculi, are treated as dynamic theories that can be combined to reason about heterogeneous systems whose components are verified using different program logics. HDL provides two key operations: Lifting extends an individual dynamic theory with new program constructs (e.g., the havoc operation or regular programs) and automatically augments its calculus with sound reasoning principles for the new constructs; and Combination enables cross-language reasoning in a single modality via Heterogeneous Dynamic Theories , facilitating the reuse of existing proof infrastructure. By lifting combined theories with regular programs, we obtain heterogeneous control structures that allow us to reason about intertwined cross-language behavior. We formalize dynamic theories, their lifting and combination, and prove the soundness of all proof rules in Isabelle. We also introduce a proof rule combining deductive DL-based reasoning with reasoning principles from Kleene Algebras with Tests. Furthermore, we prove relative completeness theorems for lifting and combination: Under usual assumptions, reasoning about lifted or combined theories is no harder than reasoning about the constituent dynamic theories and their common first-order structure (i.e., the “data theory”). We demonstrate HDL’s value by verifying an automotive case study where a Java controller (formalized in Java dynamic logic) steers a plant model (formalized in differential dynamic logic).


title: Fast Atomicity Monitoring

authors:
Hünkar Can Tunç
Yifan Dong
Andreas Pavlogiannis

abstract: Atomicity is a fundamental abstraction in concurrency, specifying that program behavior can be understood by considering specific code blocks executing atomically. However, atomicity invariants are tricky to maintain while also optimizing for code efficiency, and atomicity violations are a common root cause of many concurrency bugs. To address this problem, several dynamic techniques have been developed for testing whether a program execution adheres to an atomicity specification, most often instantiated as conflict-serializability . The efficiency of the analysis has been targeted in various papers, with the state-of-the-art algorithms RegionTrack and Aerodrome achieving a time complexity O ( n k 3 ) and O ( n k ( k + v + ℓ ) ) , respectively, for a trace σ of n events, k threads, v locations, and ℓ locks. In this paper we introduce AtomSanitizer , a new algorithm for testing conflict-serializability, with time complexity O ( n k 2 ) . AtomSanitizer operates in an efficient streaming style, is theoretically faster than all existing algorithms, and also has a smaller memory footprint. Moreover, it is the first algorithm designed to use little locking when deployed in a concurrent monitoring setting. Experiments on standard benchmarks indicate that AtomSanitizer is always faster in practice than all existing conflict-serializability testers. Finally, we also implement AtomSanitizer inside the TSAN framework, for monitoring atomicity in real time. Our experiments reveal that AtomSanitizer incurs only a marginal time and space overhead over the data-race detection engine of TSAN , and thus is the first algorithm for conflict-serializability demonstrated to be suitable for a runtime monitoring setting.


title: Verification Modulo Tested Library Contracts

authors:
Abhishek Uppar
Omar Muhammad
Sumanth Prabhu S
Deepak D'Souza
P. Madhusudan
Adithya Murali

abstract: We consider the problem of verification modulo tested library contracts as a step towards automating the verification of client programs that use complex libraries. We formulate this problem as the synthesis of modular contracts for the library methods used by the client that are adequate to prove the client correct, and that also pass the scrutiny of a testing engine that tests the library against these contracts. We also consider a new form of method contracts called contextual contracts that arise in this setting that hold in the context of the client program, and can often be simpler and easier to infer than classical modular contracts. We provide a counterexample-guided learning framework to solve this problem, in which the synthesizer interacts with a constraint solver as well as the testing engine in order to infer adequate modular/contextual method contracts and inductive invariants for the client. The main synthesis engines we use are generalizing CHC solvers that are realized using ICE learning algorithms. We realize this framework in a tool called Dualis and show its efficacy on benchmarks where clients call large libraries.


title: Compiling to Recurrent Neurons

authors:
Joey Velez-Ginorio
Nada Amin
Konrad P. Kording
Steve Zdancewic

abstract: Discrete structures are currently second-class in differentiable programming. Since functions over discrete structures lack overt derivatives, differentiable programs do not differentiate through them and limit where they can be used. For example, when programming a neural network, conditionals and iteration cannot be used everywhere; they can break the derivatives necessary for gradient-based learning to work. This limits the class of differentiable algorithms we can directly express, imposing restraints on how we build neural networks and differentiable programs more generally. However, these restraints are not fundamental. Recent work shows conditionals can be first-class, by compiling them into differentiable form as linear neurons. Similarly, this work shows iteration can be first-class—by compiling to linear recurrent neurons. We present a minimal typed, higher-order and linear programming language with iteration called Cajal ( ⊸ , 𝟚 , ℕ ) . We prove its programs compile correctly to recurrent neurons, allowing discrete algorithms to be expressed in a differentiable form compatible with gradient-based learning. With our implementation, we conduct two experiments where we link these recurrent neurons against a neural network solving an iterative image transformation task. This determines part of its function prior to learning. As a result, the network learns faster and with greater data-efficiency relative to a neural network programmed without first-class iteration. A key lesson is that recurrent neurons enable a rich interplay between learning and the discrete structures of ordinary programming.


title: Bridging Coverage and Confidence: Reliable Static False Alarm Elimination via Input-Agnosticity

authors:
Jiayi Wang
Yu Wang
Linzhang Wang
Ke Wang

abstract: Static analysis is a foundational technique for detecting software defects, yet it notoriously suffers from high false positive rates. Prior efforts to reduce false positives via model checking, symbolic execution, dynamic analysis, testing, or machine learning either fail to scale or mistakenly eliminate real defects. This paper presents Rican , a novel approach that leverages dynamic testing to reliably eliminate false alarms in static analysis. The key insight behind Rican is the concept of input-agnosticity : if the validity of an alarm is independent of program inputs along each execution path, then once all such paths from the program entry to the alarm site have been exercised by tests without triggering the alarmed bug, the alarm can be soundly classified as a false positive. To realize this insight, Rican uses a conservative input-agnosticity analysis based on data dependence to identify input-agnostic alarms among all reported alarms. However, validating even input-agnostic alarms requires exploring all feasible paths, which is generally infeasible. To address this, Rican computes a necessary set of paths by identifying only those branches and loops that may influence the alarm’s validity. Finally, Rican eliminates false alarms using existing dynamic testing and post-directed fuzzing to cover these critical paths. We evaluate Rican on six real-world open-source projects using a value-flow-based static analysis front-end. Our experiments show that Rican reliably eliminates 1,313 (45.09%) false positives out of 2,912 double-free, use-after-free, and null-pointer-dereference alarms, without eliminating any real alarms in our evaluation. In addition, Rican incurs negligible overhead beyond the data dependence computed by the underlying analysis. Our user studies further demonstrate that Rican reduces the manual effort required for alarm inspection by over 70% on average and helps programmers find bugs more quickly and accurately, highlighting its practical usefulness in real-world static analysis.


title: Redundant Array Computation Elimination

authors:
Zixuan Wang
Liang Yuan
Xianmeng Jiang
Kun Li
Junmin Xiao
Yunquan Zhang

abstract: Redundancy elimination is a key optimization direction, and loop nests are the main optimization target in modern compilers. Previous work on redundancy elimination of array computations in loop nests either targets specific computation patterns or fails to recognize redundancies with complex structures. This paper proposes RACE (Redundant Array Computation Elimination), a hash-based technique that utilizes a novel two-level scheme to identify the data reuse between array references and the computation redundancies between expressions, enabling hierarchical redundancy detection beyond pattern-specific methods. It traverses the expression trees in loop nests to detect redundancies hierarchically in linear time and generates efficient code with optimized auxiliary arrays that store redundant computation results. Furthermore, RACE supports the expression reassociation with various aggressive strategies to improve the redundancy opportunities. Experimental results demonstrate the effectiveness of RACE.


title: Pantomime: Constructive Leakage Proofs via Simulation

authors:
Robin Webbers
Robert Schenck
Wind Wong
Kristina Sojakova
Klaus von Gleissenthall

abstract: Tools for verifying leakage descriptions of hardware aim to ensure that a given hardware design doesn’t leak secrets via its microarchitecture, when executing programs with appropriate countermeasures. However, existing techniques for proving correctness of leakage descriptions are based on non-constructive proofs via non-interference. As a result, they often rely on expensive solvers that offer little help when verification fails or require handwritten invariants, which are difficult to come up with and even harder to debug. In this paper, we present a new approach to leakage verification which we call simulation-based leakage proofs . To show that a leakage description correctly captures a hardware design using a simulation-based proof, the user constructs a simulator—another hardware design that must faithfully replicate all attacker-observable behavior from explicitly leaked secrets. Simulation-based proofs therefore offer a constructive alternative to classic non-interference proofs, exposing a proof object—the simulator, witnessing the correctness claim. As simulators are just programs, we can write, execute and debug them like any other program, making them easy to use. We also show that they can be checked locally, which makes proof checking fast. We implement simulation-based leakage proofs in P ANTOMIME , a tool that supports writing processors and their leakage proofs in Haskell; we report on using Pantomime to write and verify AIM Core , a 5-stage in-order processor, its leakage description, and simulator, as well as a side-channel hardened version of the core. We show that Pantomime verifies them efficiently (it checks AIM Core in under 40s), and use AIMCore’s leakage description to check for leakages in crypto libraries which uncovered two new vulnerabilities in wolfSSL that have both been assigned CVE’s.


title: Path-Sensitive Abstract Interpretation for WCET Estimation

authors:
Shangshang Xiao
Mengxia Sun
Wei Zhang
Naijun Zhan
Lei Ju

abstract: Worst-Case Execution Time (WCET) analysis provides an upper bound on a program’s execution time and is fundamental to the design and verification of real-time systems. Accurate modeling of cache behavior is critical for WCET estimation, as cache-miss latency is typically orders of magnitude larger than cache-hit latency. Since cache behavior is path dependent, existing methods commonly use abstract interpretation to estimate cache behaviors without enumerating all paths. However, conventional abstract interpretation is context-agnostic—adopting the most conservative case across paths—and thus may produce an overestimated WCET bound. To bridge the gap between scalability and accuracy, we propose a path-sensitive abstract-interpretation-based cache analysis that maintains a set of cache states drawn from critical execution paths to derive context-aware cache behavior. This path-sensitive cache analysis integrates seamlessly into standard WCET frameworks, resulting in tight yet provably sound WCET bounds. Experiments show that our approach improves WCET accuracy by an average of 24.83% without sacrificing scalability.


title: Equality Saturation for Quantum Circuit Optimization

authors:
Ganxiang Yang
Paige Raun
Runzhou Tao
Ronghui Gu

abstract: Optimizing a quantum circuit is hard because it requires exploring a vast space of functionally equivalent circuits, produced by applying local circuit rewrites such as gate cancellation and commutation. Each additional rewrite can exponentially expand the space of equivalent circuits, so existing optimizers can only explore a tiny fraction of this space and often produce suboptimal results. We present Quasar , a new quantum circuit optimizer that can generate a step-limited optimal circuit: given a bound on rewrite iterations, it returns the lowest-cost circuit reachable within that bound. To achieve this, Quasar constructs two complementary e-graphs for the quantum circuit’s graph and sequence representations. Quasar then infers an atomic rewrite set for application on both e-graphs, which improves optimization performance by orders of magnitude. Finally, Quasar employs a series of new optimization techniques to ensure both soundness and scalability of equality saturation on quantum circuits. Across standard benchmarks, Quasar achieves geometric-mean reductions of 20.2% in 2-qubit gate count, 33.5% in total gate count, and 24.2% in circuit depth, and a 21.4% fidelity improvement over unoptimized circuits, outperforming or matching state-of-the-art rewrite-based optimizers on 75%, 92%, 62%, and 80% of circuits, respectively.


title: Verification of Recursively Defined Quantum Circuits

authors:
Mingsheng Ying
Zhicheng Zhang

abstract: Recursive techniques have recently been introduced into quantum programming so that a variety of large quantum circuits and algorithms can be elegantly and compactly programmed. In this paper, we present a proof system for formal verification of the correctness of recursively defined quantum circuits. The soundness and (relative) completeness of the proof system are established. To demonstrate its effectiveness, we present a series of application examples, including formal verification of multi-qubit controlled gates, a quantum circuit for generating multi-qubit GHZ (Greenberger-Horne-Zeilinger) states, and more sophisticated quantum algorithms with recursive structures such as the quantum Fourier transform, quantum state preparation, and quantum random access memories (QRAMs).


title: SAQR-QC: A Logic for Scalable but Approximate Quantitative Reasoning about Quantum Circuits

authors:
Nengkun Yu
Jens Palsberg
Thomas Reps

abstract: Reasoning about quantum programs remains a fundamental challenge, regardless of the programming model or computational paradigm. Existing verification techniques are insufficient—even for quantum circuits, a deliberately restricted model that lacks classical control, but still underpins many current quantum algorithms. Many existing formal methods require exponential time and space to represent and manipulate (representations of) assertions and judgments, making them impractical for quantum circuits with many qubits. This paper presents SAQR-QC, a logic for S calable but A pproximate Q uantitative R easoning about Q uantum C ircuits. SAQR-QC has three characteristics: (i) some deliberate loss of precision is built into it; (ii) it has a mechanism to help the accumulated loss of precision during a sequence of reasoning steps remain small; and (iii) every reasoning step is local—involving just a small number of qubits—making reasoning scalable. We demonstrate the effectiveness of SAQR-QC via two case studies: the verification of GHZ circuits involving non-Clifford gates, and the analysis of quantum phase estimation—a core subroutine in Shor’s factoring algorithm.


title: Cobble: Compiling Block Encodings for Quantum Computational Linear Algebra

abstract: Quantum algorithms for computational linear algebra promise up to exponential speedups for applications such as simulation and regression, making them prime candidates for hardware realization. But these algorithms execute in a model that cannot efficiently store matrices in memory like a classical algorithm does, instead requiring developers to implement complex expressions for matrix arithmetic in terms of correct and efficient quantum circuits. Among the challenges for the developer is navigating a cost model in which conventional optimizations for linear algebra, such as subexpression reuse, can be inapplicable or unprofitable. In this work, we present Cobble, a language for programming with quantum computational linear algebra. Cobble enables developers to express and manipulate the quantum representations of matrices, known as block encodings, using high-level notation that automatically compiles to correct quantum circuits. Cobble features analyses that compute the time and space usage of programs, as well as optimizations that reduce overhead and generate efficient circuits using state-of-the-art techniques such as the quantum singular value transformation. We evaluate Cobble on benchmark kernels for simulation, regression, search, and other applications, showing 2.6×−25.4× speedups on these benchmarks compared to the unoptimized baseline.


title: Incremental Computation for Efficient Programmable Inference in Probabilistic Programs

authors:
Fabian Zaiser
Jack Czenszak
Martin C. Rinard
Vikash K. Mansinghka
Alexander K. Lew

abstract: Inference in probabilistic programs generally requires evaluating many possible program executions to find those of high posterior density. To scale inference to large datasets, it is crucial that expensive intermediate results are shared across these many evaluations, rather than recomputed from scratch. This paper presents a new approach to realizing this sharing, based on incremental computation , a technique for efficiently recomputing (deterministic) program outputs when program inputs change. First, we show how expressive probabilistic programs can be compiled to deterministic ones that compute their density functions. Then, building on the incremental λ -calculus, we develop a general technique for compositionally incrementalizing expressive functional programs, and apply it to these densities. The resulting incremental densities can be used to accelerate a broad range of Monte Carlo inference algorithms, including for nonparametric models not well supported by existing systems. Furthermore, our decomposition of incremental density computation into separate density and incrementalization steps allows for modular reasoning about correctness—a key pain point in existing systems, where ad-hoc incrementalization features are a known source of soundness bugs. We develop denotational logical relations arguments for the correctness of each step independently, and implement the approach in a Julia prototype, finding that it leads to asymptotic runtime improvements in the size of the dataset on a range of models and inference algorithms.


title: Optimal Predicate Pushdown Synthesis

authors:
Robert Zhang
Eric Hayden Campbell
Dixin Tang
Isil Dillig

abstract: Predicate pushdown is a long-standing performance optimization that filters data as early as possible in a computational workflow. In modern data pipelines, this transformation is especially important because much of the computation occurs inside user-defined functions (UDFs) written in general-purpose languages such as Python and Scala. These UDFs capture rich domain logic and complex aggregations and are among the most expensive operations in a pipeline. Moving filters ahead of such UDFs can yield substantial performance gains, but doing so requires semantic reasoning. This paper introduces a general semantic foundation for predicate pushdown over stateful fold-based computations. We view pushdown as a correspondence between two programs that process different subsets of input data, with correctness witnessed by a bisimulation invariant relating their internal states. Building on this foundation, we develop a sound and relatively complete framework for verification, alongside a synthesis algorithm that automatically constructs optimal pushdown decompositions by finding the strongest admissible pre-filters and weakest residual post-filters. We implement this approach in a tool called Pusharoo and evaluate it on 150 real-world pandas and Spark data-processing pipelines. Our evaluation shows that Pusharoo is significantly more expressive than prior work, producing optimal pushdown transformations with a median synthesis time of 1.6 seconds per benchmark. Furthermore, our experiments demonstrate that the discovered pushdown optimizations speed up end-to-end execution by an average of 2.4× and up to two orders of magnitude.


title: Scalable Floating-Point Satisfiability via Staged Optimization

authors:
Yuanzhuo Zhang
Zhoulai Fu
Binoy Ravindran

abstract: This work introduces StageSAT , a new approach to solving floating-point satisfiability that bridges SMT solving with numerical optimization. StageSAT reframes a floating-point formula as a series of optimization problems in three stages, each with increasing precision. It begins with a fast, projection-aided descent objective to efficiently guide the search toward a feasible region, then proceeds to bit-level accuracy with units-in-the-last-place ( ULP ) 2 optimization and a final n -ULP lattice refinement to ensure correctness. By construction, the final two stages use a representing function that evaluates to zero if and only if a candidate satisfies all constraints. Thus, whenever optimization drives the bit-precise objective to zero, the resulting assignment is a valid solution, providing a built-in guarantee of soundness (no spurious SAT results). To further improve the search, StageSAT introduces a partial monotone descent property on linear constraints via an orthogonal projection technique, which prevents the optimizer from stalling on flat or misleading objective landscapes. Critically, this solver requires no heavy bit-level reasoning or specialized abstractions of floating-point arithmetic; it treats complex arithmetic as a black box, using runtime evaluations to navigate the input space. We implement StageSAT and evaluate it on extensive benchmarks, including the SMT-COMP’25 floating-point suites and difficult cases from prior work. In our experiments, StageSAT proved both more scalable and more accurate than state-of-the-art optimization-based alternatives. It solved strictly more formulas than any competing solver under the same time budget – in fact, StageSAT found most of the satisfiable instances in our benchmarks and never produced a spurious model for an unsatisfiable formula. This amounts to 99.4 % recall on satisfiable cases with 0 % false SAT in our benchmarks, exceeding the reliability of prior optimization-based solvers we tested. StageSAT also delivered significant speedups (often 5 − 10 × faster) over traditional bit-precise SMT solvers and earlier numeric solvers. These results demonstrate that our staged optimization strategy can significantly improve both the performance and correctness of floating-point satisfiability solving.


title: A Formally Verified Foundation for Compositional Heterogeneous Coherence

authors:
An Qi Zhang
Andrés Goens
Daniel J. Sorin
Vijay Nagarajan

abstract: Modern processors integrate heterogeneous devices to expose unified shared memory. Yet, the de-facto design pattern used to compose their disparate coherence protocols lacks a formal foundation. This leaves the door open for subtle consistency bugs, in a critical gap between practice and correctness. This paper provides the first formal, machine-checked proof that a de-facto design pattern, which we call the Principle of Synchronous Propagation, is correct. Leveraging a new unifying abstraction for coherence protocols, our central theorem (machine checked in Lean) proves that Synchronous Propagation is sufficient to guarantee the Compound Memory Consistency Model for a wide class of protocols. Our work provides long-needed assurance for current designs and delivers a reusable, compositional framework for verifying future heterogeneous systems.


title: Causality and Semantic Separation

authors:
Anna Zhang
Qinglan Luo
London Bielicke
Eunice Jun
Adam Chlipala

abstract: The design of scientific experiments deserves its own variation of formal verification to catch cases where scientists made important mistakes, such as forgetting to take confounding variables into account. One of the most fundamental underpinnings of science is causality , or what it means for interventions in the world to cause other outcomes, as formalized by computer scientists like Judea Pearl. However, these ideas had not previously been made rigorous to the standards of the programming-languages community, where one expects a (syntactic) program analysis to be proved sound with respect to a natural semantics. In the domain of causality, as the relevant “program analysis,” we focus on d- separation , a classic condition on graphs that can be used to decide when the design of an experiment controls for sufficiently many confounding variables, even though the reason that this condition works is often unintuitive. Our central result (mechanized in Rocq) is that d -separation exactly coincides with a novel semantic definition inspired by noninterference from the theory of security. This characterization provides a structural semantic foundation for d -separation and helps explain why the graph-theoretic condition is correct, independently of probabilistic assumptions. For each given automated test on the quality of an experiment design, our theorem justifies an associated method for falsifying the world-modeling hypothesis behind the experiment.


title: Neptune: Advanced ML Operator Fusion for Locality and Parallelism on GPUs

authors:
Yifan Zhao
Egan Johnson
Prasanth Chatarasi
Vikram S. Adve
Sasa Misailovic

abstract: Operator fusion has become a key optimization for deep learning, which combines multiple deep learning operators to improve data reuse and reduce global memory transfers. However, existing tensor compilers struggle to fuse complex reduction computations involving loop-carried dependencies, such as attention mechanisms. This paper introduces Neptune, a tensor compiler for advanced operator fusion for sequences of reduction operators. Neptune presents a new approach for advanced operator fusion, which intentionally breaks some existing dependencies and compensates by constructing algebraic correction expressions that allow the kernel to produce the correct result. Applying Neptune’s advanced operator fusion to a plain attention operator generates operators equivalent to FlashAttention and FlashDecoding. On ten attention-based benchmarks, Neptune, starting from a plain attention code and a high–level scheduling template, outperforms existing compilers like Triton, TVM, and Flex Attention, including Triton–based implementations of FlashAttention. Across four different GPU architectures from NVIDIA and AMD, Neptune–generated kernels have an average speedup of 1.35× over the next best alternative, with up to 2.65 × speedup on Nvidia GPUs and up to 3.32 × on AMD GPUs, demonstrating its effectiveness for deep learning workloads.


title: Trace-Guided Synthesis of Effectful Test Generators

authors:
Zhe Zhou
Ankush Desai
Benjamin Delaware
Suresh Jagannathan

abstract: Several recently proposed program logics have incorporated notions of under approximation into their design, enabling them to reason about reachability rather than safety. In this paper, we explore how similar ideas can be integrated into an expressive type and effect system. We use the resulting underapproximate type specifications to guide the synthesis of test generators that probe the behavior of effectful black-box systems. A key novelty of our type language is its ability to capture underapproximate behaviors of effectful operations using symbolic traces that expose latent data and control dependencies, constraints that must be preserved by the test sequences the generator outputs. We implement this approach in a tool called Clouseau, and evaluate it on a diverse range of applications by integrating Clouseau’s synthesized generators into property-based testing frameworks like QCheck and model-checking tools like P. In both settings, the generators synthesized by Clouseau are significantly more effective than the default testing strategy, and are competitive with state-of-the-art, handwritten solutions.


title: EREQ: Regular Expressions with Quantifiers and Incremental Quantifier Elimination

authors:
Ekaterina Zhuchko
Ian Erik Varatalu
Margus Veanes
Nikolaj S. Bjørner

abstract: Weak monadic second-order logic ( wMSO ) is a foundational tool for specifying regular properties. Traditional decision procedures for this logic typically translate wMSO formulas into finite automata. Although the logic is decidable, this approach incurs non-elementary complexity in the worst-case. Nearly thirty years ago, the state-of-the-art MONA tool showed that, despite these theoretical limits, wMSO can be decided efficiently in practice through carefully optimized automata constructions. We revisit wMSO from an algebraic perspective by introducing Extended Regular Expressions with Quantifiers ( EREQ ). Instead of relying on automata determinization, EREQ employs symbolic derivatives to perform incremental quantifier elimination, providing a compositional and symbolic alternative to classical automata-based approaches. We present a linear-time translation of wMSO into EREQ and a derivative-based decision procedure for EREQ . We prove the correctness of the translation and of the derivative construction in the Lean proof assistant. We implement our approach in Rust and evaluate it on a set of established MONA benchmarks, demonstrating competitive performance with state-of-the-art tools. Our results demonstrate the potential of derivative-based methods, opening new avenues for efficient decision procedures in EREQ .


title: Synthesizing Backward Error Bounds, Backward

authors:
Laura Zielinski
Justin Hsu

abstract: Backward stability is a desirable property for a well-designed numerical algorithm: given an input, a backward stable floating-point program produces the exact output for a nearby input. While automated tools for bounding the forward error of a numerical program are well-established, few existing tools target backward error analysis. We present a formal framework that enables sound, automated backward error analysis for a broad class of numerical programs. First, we propose a novel generalization of the definition of backward stability that is both compositional and flexible, satisfied by a wide range of floating-point operations. Second, based on this generalization, we develop the category Shel where morphisms model stable numerical programs, and show that structures in Shel support a rich variety of backward error analyses. Third, we implement a tool, eggshel , that automatically searches within a syntactic subcategory of Shel to prove backward stability for a given program. Our algorithm handles many programs with variable reuse, a known challenge in backward error analysis. We prove soundness of our algorithm and use our tool to synthesize backward error bounds for a suite of programs that were previously beyond the reach of automated analysis.


venue: popl

title: Deterministic Parsing of Ambiguous Grammars

authors:
Alfred V. Aho
Stephen C. Johnson
Jeffrey D. Ullman

abstract: We consider methods of describing the syntax of programming languages in ways that are more flexible and natural than conventional BNF descriptions. These methods involve the use of ambiguous context-free grammars together with rules to resolve syntactic ambiguities. We show how efficient LL and LR parsers can be constructed directly from certain classes of these specifications.


title: Programming Language Semantics and Closed Applicative Languages

abstract: This paper proposes axioms to define a sequence of language-classes; the most general is that of "programming language", the most restricted has some simple and attractive properties. Here "language" is used in its traditional sense as referring to a set of interpreted expressions. We are concerned with the syntax of an expression only to the degree needed to relate its structure to its "meaning". A clear distinction is drawn between a "language" and the many possible "realizations" of that language.This introduction comprises a survey and opinionated discussion of the contents of the paper, therefore the reader who wishes to get on with the technical exposition can skip to the next section.


title: On the Definitional Method of Standard PL/1

abstract: In order to define the semantics of PL/I in a form which is both precise and readable, a method of definition has been developed which employs an abstract machine operating on tree-structured data. The classes of trees involved are defined by formal grammars, while the algorithms governing the behaviour of the machine are expressed semi-formally in prose. This algorithmic metalanguage is itself intended to have largely intuitive semantics, but these are made more precise by an indication of how they could be supported at a lower level of detail within the abstract machine.


title: On the Decision Problems of Program Schemas with Commutative and Invertable Functions

abstract: We consider partially interpreted monadic schemas in which some functions are specified to commute, or some function is specified to be invertible. The decision problems considered are those of halting, divergence, equivalence, inclusion and isomorphism. It is shown that with either commutativity or invertibility alone, all these decision problems are solvable, whereas with both commutativity and invertibility, all become unsolvable. These results are also related to the decision problems for finite automata on multi-dimensional infinite tapes.


title: Mode Modules as Representations of Domains

authors:
Alice E. Fischer
Michael J. Fischer

abstract: High level programming languages tend to free a programmer from concern about the underlying machine structure and permit him to talk about his problem domain in more direct terms. Thus, he may imagine that objects such as real numbers, character strings, and linear arrays really exist in the machine as atomic entities and he need not understand the details of how they are actually represented in the machine. Of course what distinguishes various kinds of objects are the operations that may be performed on them, so when talking about the domain of real numbers, we should include the basic arithmetic operations and constants, and for strings, operations such as length, concatenation and indexing.Unfortunately, existing languages do not permit a programmer to ignore completely questions of representation, for if his problem domain does not happen to be included already in the repertoire of domains supported by the language, the programmer must figure out a representation himself and remember it throughout his programming effort. For example, a FORTRAN programmer may know that it is not meaningful to multiply two integers that happen to represent insurance policy numbers, but he has no way of informing the compiler of this fact.Many extensible languages do provide a wide range of data types including structured types, enabling a programmer to choose a more natural representation of his external objects, but the structured data types reflect only the structure of the data, not its meaning. They still provide only one natural representation for both integers and dates, mass and speed, or planar vectors in cartesian or polar coordinates.Many domains that arise in practice have a great deal of similarity between them which one must employ in his programs. For example, the domain of length 3 vectors and the domain of length 4 vectors have the "same" rule of addition, that is, add componentwise, and it would be onerous to have to repeat this information for each new length vector. Thus, one needs both the ability to define brand new domains and also a method for expressing relations among them.We present here some mechanisms, collectively called Aleph-1, which allow the expansion of a programming language's repertoire of internal domains. Many of the ideas embodied in Aleph-1 have been described previously in the literature, and we acknowledge their influence on our thinking, in particular the work of Balzer [1] and Reynolds [5] suggesting the utility of separating out the abstract behavior of an object from its representation, the languages Pascal [10] and Simula-67 [3] which associate functions with data types and types with alternate representations, modular generic functions in Basel [2], Standish's wide variety of structured data [6], and the systematic (though not extensible) treatment of coercion in Algol-68 [8]. Our domain mechanisms bear certain strong similarities to those developed by Morris for the purposes of protection [4].


title: Strict Deterministic Versus LR(0) Parsing

authors:
Matthew M. Geller
Michael A. Harrison

abstract: Recently strict deterministic grammars and languages have been introduced [9,10,11]. This family of languages is quite fundamental in the study of the mathematical properties of deterministic languages and in dealing with some classical families of grammars such as LR(k) and bounded right context grammars [7,8,14]. These grammars are closely related to LR(0) grammars [1,12,13,14], in fact each strict deterministic grammar is also LR(0). In the present paper, we consider the question of how to parse strict deterministic grammars. We introduce part of a more general theory called "characteristic LR(k) parsing". This actually produces parsers which are tuned to the characteristics of a particular family of grammars. We apply the theory to the family of strict deterministic grammars and we get parsers which are as fast as canonical LR(k) parsers but are substantially smaller. They are not necessarily minimal but we postpone any discussion of minimality to the sequel.The techniques used in the present discussion are quite general [5]. For instance, the study in [3] is similar in spirit to our technique. The optimization techniques for LR(k) parsers in [2] do not work in the case k = 0 without modification. After modifying those methods for k = 0, it can be shown that our parsers cannot be produced by those techniques. This fact has its positive aspect in that our parsers may be smaller and its negative aspect in that error detection may be delayed.The present paper is divided into the present introduction and three sections. In the remainder of this introduction, some basic definitions of strict deterministic and LR(k) parsing are given. We have tried to follow [1] as much as possible in order to minimize the amount of new material to be absorbed. The order of the results is the order needed to prove that the characteristic parser works. In Section III, we apply the theory of Section II to strict deterministic parsing. A simple example shows that the new parsers can be unboundedly smaller than the canonical LR(0) parser.The present paper is meant to be an extended abstract and no proofs are included.The rest of the introduction is concerned with notational conventions for the technical concepts needed.


title: Practical Syntactic Error Recovery

authors:
Susan L. Graham
Steven P. Rhodes

abstract: A substantial portion of any programmer's time is spent in debugging. One of the major services of any compiler ought to be to provide as much information as possible about compile-time errors in order to minimize the time required for debugging. A good error detection and recovery scheme should maximize the number of errors detected but minimize the number of times it reports an error when there is none. These spurious error detections and their associated error messages are usually engendered by an inappropriate recovery action.In this paper we describe a recovery scheme for syntax errors which provides high quality recovery with good diagnostic information at relatively low cost. In addition, implementation of the recovery scheme can be automated - that is, the recovery routine can be created by a parser-generator. Therefore, the compiler designer need not be burdened with the difficulties of error recovery and the programming effort necessary to design and debug a myriad of ad hoc recovery routines.


title: Analysis of a Simple Algorithm for Global Flow Problems

authors:
Matthew S. Hecht
Jeffrey D. Ullman

abstract: There is an ordering of the nodes of a flow graph G which topologically sorts the dominance relation and can be found in 0(edges) steps. This ordering is the reverse of the order in which a node is last visited while growing any depth-first spanning tree of G. Moreover, if G is reducible, then this ordering topologically sorts the dag of G. Thus, for a reducible flow graph (rfg) there is a simple algorithm to compute the dominators of each node in 0(edges) bit vector steps.The main result of this paper relates two parameters of an rfg. If G is reducible, d is the largest number of back edges found in any cycle-free path in G, and k is the length of the interval derived sequence of G, then k≥d. From this result it follows that there is a very simple bit propagation algorithm (indeed, the obvious one) which also uses the above ordering, and is at least as good as the interval algorithm for solving all known global data flow problems such as available expressions and live variables.


title: Actor Induction and Meta-Evaluation

authors:
Carl Hewitt
Peter Boehler Bishop
Irene Greif
Brian Cantwell Smith
Todd Matson
Richard Steiger

abstract: The PLANNER project is continuing research in natural and effective means for embedding knowledge in procedures. In the course of this work we have succeeded in unifying the formalism around one fundamental concept: the ACTOR. Intuitively, an ACTOR is an active agent which plays a role on cue according to a script. We use the ACTOR metaphor to emphasize the inseparability of control and data flow in our model. Data structures, functions, semaphores, monitors, ports, descriptions, Quillian nets, logical formulae, numbers, identifiers, demons, processes, contexts, and data bases can all be shown to be special cases of actors. All of the above are objects with certain useful modes of behavior. Our formalism shows how all of these modes of behavior can be defined in terms of one kind of behavior: sending messages to actors. An actor is always invoked uniformly in exactly the same way regardless of whether it behaves as a recursive function, data structure, or process.


title: A Unified Approach to Global Program Optimization

abstract: A technique is presented for global analysis of program structure in order to perform compile time optimization of object code generated for expressions. The global expression optimization presented includes constant propagation, common subexpression elimination, elimination of redundant register load operations, and live expression analysis. A general purpose program flow analysis algorithm is developed which depends upon the existence of an "optimizing function." The algorithm is defined formally using a directed graph model of program flow structure, and is shown to be correct. Several optimizing functions are defined which, when used in conjunction with the flow analysis algorithm, provide the various forms of code optimization. The flow analysis algorithm is sufficiently general that additional functions can easily be defined for other forms of global code optimization.


title: Large Scale File Processing - Pogol

abstract: Article Free Access Share on Large scale file processing: POGOL Author: Gloria J. Lambert Dept. of Defense Dept. of DefenseView Profile Authors Info & Claims POPL '73: Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languagesOctober 1973Pages 226–234https://doi.org/10.1145/512927.512948Published:01 October 1973Publication History 0citation377DownloadsMetricsTotal Citations0Total Downloads377Last 12 Months60Last 6 weeks2 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


title: Recursively Defined Data Types

authors:
Clayton H. Lewis
Barry K. Rosen


title: Procedure Linkage Optimization

authors:
Andrea Maggiolo-Schettini
Barry K. Rosen
H. Raymond Strong

abstract: This paper discusses the desirability of procedure linkage optimization and sketches a general theory of interpretive semantics which is motivated by technical problems in specifying and validating program transformations that optimize procedure linkages. One particular transformation is treated in detail.Recursive ALGOL 60 procedures sometimes pass parameters by name in such a way that the general thunk mechanism is unnecessary and inefficient. We present an optimization which detects this kind of call-by-name and implements it thunklessly. We prove that the transformation preserves semantics and we discuss the effect on running time and memory management.


title: Types are Not Sets

abstract: The title is not a statement of fact, of course, but an opinion about how language designers should think about types. There has been a natural tendency to look to mathematics for a consistent, precise notion of what types are. The point of view there is extensional: a type is a subset of the universe of values. While this approach may have served its purpose quite adequately in mathematics, defining programming language types in this way ignores some vital ideas. Some interesting developments following the extensional approach are the ALGOL-68 type system [vW], Scott's theory [S], and Reynolds' system [R]. While each of these lend valuable insight to programming languages, I feel they miss an important aspect of types.Rather than worry about what types are I shall focus on the role of type checking. Type checking seems to serve two distinct purposes: authentication and secrecy. Both are useful when a programmer undertakes to implement a class of abstract objects to be used by many other programmers. He usually proceeds by choosing a representation for the objects in terms of other objects and then writes the required operations to manipulate them.


title: Advice on Structuring Compilers and Proving Them Correct

abstract: The purpose of this paper is to advise an approach (and to support that advice by discussion of an example) towards achieving a goal first announced by John McCarthy: that compilers for higher-level programming languages should be made completely trustworthy by proving their correctness. The author believes that the compiler-correctness problem can be made much less general and better-structured than the unrestricted program-correctness problem; to do so will of course entail restricting what a compiler may be.


title: Formalization of Exel

authors:
Louis Nolin
G. Ruggiu


title: Top Down Operator Precedence

abstract: Article Free Access Share on Top down operator precedence Author: Vaughan R. Pratt Massachusetts Institute of Technology Massachusetts Institute of TechnologyView Profile Authors Info & Claims POPL '73: Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languagesOctober 1973 Pages 41–51https://doi.org/10.1145/512927.512931Online:01 October 1973Publication History 25citation3,168DownloadsMetricsTotal Citations25Total Downloads3,168Last 12 Months170Last 6 weeks70 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


title: Transitions in Extendible Arrays

abstract: Arrays are among the best understood and most widely used data structures. Yet even now, there are no satisfactory techniques for handling algorithms involving extendible arrays (where, e.g., rows and/or columns can be added dynamically). In this paper, the problem of allocating storage for extendible arrays is examined in the light of our earlier work on data graphs and addressing schemes. A formal analog of the assertion that simplicity of array extension precludes simplicity of transition (marching along rows/columns) is proved.


title: Labelled Precedence Parsing

abstract: Precendece techniques have been widely used in the past in the construction of parsers. However, the restrictions imposed by them on the grammars were hard to meet. Thus, alteration of the rules of the grammar was necessary in order to make them acceptable to the parser. We have shown that, by keeping track of the possible set of rules that could be applied at any one time, one can enlarge the class of grammars considered. The possible set of rules to be considered is obtained directly from the information given by a labelled set of precedence relations. Thus, the parsers are easily obtained. Compared to the precedence parsers, this new method gives a considerable increase in the class of parsable grammars, as well as an improvement in error detection. An interesting consequence of this approach is a new decomposition technique for LR parsers.


title: Mathematical Semantics of Snobol 4

abstract: This paper analyzes the semantics of the programming language SNOBOL4, following the mathematical approach proposed by D. Scott and C. Strachey. The study aims at clarifying a rather unusual semantic structure, and at demonstrating that the mathematical approach can provide a natural and usable formal specification of a practical programming language.


title: Reasoning About Programs

authors:
Richard J. Waldinger
Karl N. Levitt

abstract: This paper describes a theorem prover that embodies knowledge about programming constructs, such as numbers, arrays, lists, and expressions. The program can reason about these concepts and is used as part of a program verification system that uses the Floyd-Naur explication of program semantics. It is implemented in the QA4 language; the QA4 system allows many bits of strategic knowledge, each expressed as a small program, to be coordinated so that a program stands forward when it is relevant to the problem at hand. The language allows clear, concise representation of this sort of knowledge. The QA4 system also has special facilities for dealing with commutative functions, ordering relations, and equivalence relations; these features are heavily used in this deductive system. The program interrogates the user and asks his advice in the course of a proof. Verifications have been found for Hoare's FIND program, a real-number division algorithm, and some sort programs, as well as for many simpler algorithms. Additional theorems have been proved about a pattern matcher and a version of Robinson's unification algorithm.


title: A Parallel Approach to Compilation

abstract: Returning to the question of the definition of a to logical records.This includes removing vectorized compiler, the general problem is to find successive transformations which can be applied to large portions of the input program, translating and reducing it, step by step to a machine code representation.Compilation is no longer the process of recognizing an occurrence of a condition in a given state and taking some appropriate action.Instead the compiler needs to recognize all occur-rences of some condition in a given state and take the appropriate action.This approach to compiling was quite successful for lexical analysis and symbol table organization.The problems involved in parsing and code generation met with varying degrees of success and frustration.These problems are much more


title: A Semantic Model for Parallel Systems with Scheduling

abstract: This paper presents a semantic model for parallel systems with a scheduling mechanism that is useful for expressing and proving a wider range of properties than semantic models that do not consider scheduling.We formally describe a number of properties related to scheduling and deadlock, including "Fairness" and "Fullness", and show that schedulers with these properties behave in desirable ways.Lastly, we prove and conjecture some proof rules for scheduled systems and outline briefly the relation of this work to modelling protection in parallel systems.


title: An Assertion Language for Data Structures

authors:
Stephen A. Cook
Derek C. Oppen

abstract: In this paper we wish to consider the problem of proving assertions about programs that construct and alter arbitrarily complex data structures. In recent years several papers have been written on the subject of proving assertions about such programs; however, the class of data structures considered has generally been a proper sub-class of the class of all data structures, such as the classes of linear lists or trees. [Burstall 1972] discusses the problem of what he calls Distinct Non-repeating Lists and Distinct Non-repeating Trees. [Kowaltowski 1973] extends Burstall's approach. His approach is likewise basically tree-oriented but is applicable to more general data structures. [Laventhal 1974] restricts his attention to 'simple singly-linked lists', noting the problem of providing 'a complete framework for correctness proofs' if one attempts to handle very general data structures. [Morris 1972] discusses the question of designing a programming language for general data structures in order to facilitate verification of programs written in such a language. [Standish 1973] provides a set of axioms for the class of data structures in which, for instance, two data structures are equal iff they are component-wise equal.


title: Application of Lattice Algebra to Loop Optimization

authors:
Amelia C. Fong
John B. Kam
Jeffrey D. Ullman

abstract: Article Free Access Share on Application of lattice algebra to loop optimization Authors: Amelia Fong Princeton University, Princeton N. J. Princeton University, Princeton N. J.View Profile , John Kam Princeton University, Princeton N. J. Princeton University, Princeton N. J.View Profile , Jeffrey Ullman Princeton University, Princeton N. J. Princeton University, Princeton N. J.View Profile Authors Info & Claims POPL '75: Proceedings of the 2nd ACM SIGACT-SIGPLAN symposium on Principles of programming languagesJanuary 1975 Pages 1–9https://doi.org/10.1145/512976.512977Online:01 January 1975Publication History 13citation241DownloadsMetricsTotal Citations13Total Downloads241Last 12 Months8Last 6 weeks4 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


title: Correctness-Preserving Program Transformations

abstract: This paper extends the predicate calculus formalization of the partial correctness properties of programs (Ki, Go) to include the preservation of correctness under program transformations. The general notion of "program transformations which preserve properties" is fundamental to the theory of programming and programming languages. In the context of proofs of program correctness, transformations which preserve correctness can be used to improve less efficient, but easier to prove, programs. The basic argument in the use of correctness-preserving program transformations (hereafter CPTs) is:Assume that G is a program (with attached assertions) which has been proved correct with respect to some input-output relation Ain-Aout. Now suppose that S is some part of G, e.g. an expression, assertion, statement, etc., which is to be replaced by some other such part S' to produce the program G'. The goal is to prove that G' is also correct with respect to Ain-Aout and therefore the replacement preserves overall program correctness. Moreover, if the replacement has only a local effect, e.g. the body of a loop, then the proof of correctness-preservation should be restricted to that part of the program affected by the replacement.Section 2 reviews the current paradigm for proving program correctness. An example in section 3 illustrates CPTs in a sequence of improvements on a correct and simple, but inefficient, initial program. In section 4, the formalization of partial correctness properties of programs is recast as a semantic language definition using Knuth's semantic method (Kn1). This formalization is then used in section 5 to describe the mechanics of performing CPTs. In section 6, several questions about the formalization of sections 4 and 5 are discussed and a generalization is proposed. Finally, section 7 returns to a concrete example and suggests that the most effective use of CPTs is by identification of schematic forms. Related work is mentioned in section 8.


title: Structured Exception Handling

abstract: In this paper, we define what exception conditions are, discuss the requirements exception handling language features must satisfy, survey and analyze existing approaches to exception handling, and propose some new language features for dealing with exceptions in an orderly and reliable way. Our objective is not solely to put forward a language proposal. It is also to analyze exception handling issues and principles in detail. The proposed language features serve to highlight exception handling issues by showing how deficiencies in current approaches could be remedied in a coherent and orderly way.


title: A Fast and Usually Linear Algorithm for Global Flow Analysis

authors:
Susan L. Graham
Mark N. Wegman

abstract: A new algorithm for global flow analysis on reducible graphs is presented. The algorithm is shown to treat a very general class of function spaces. For a graph of e edges, the algorithm has a worst case time bound of 0(e log2e) function operations. In programming terms, the number of operations is shown to be proportional to e + the number of exit nodes from program loops. Consequently a restriction to one-entry one-exit control structures guarantees linearity. It is shown that by relaxing these time bounds, a yet wider class of function spaces can be handled.


title: Actor Semantics of Planner-73

authors:
Irene Greif
Carl Hewitt

abstract: Work on PLANNER-73 and actors has led to the development of a basis for semantics of programming languages. Its value in describing programs with side-effects, parallelism, and synchronization is discussed. Formal definitions are written and explained for sequences, cells, and a simple synchronization primitive. In addition there is discussion of the implications of actor semantics for the controversy over elimination of side-effects.


title: An Algebra of Relations for Machine Computation

authors:
Patrick A. V. Hall
Peter Hitchcock
Stephen Todd

abstract: This paper extends the relational algebra of data bases, presented by Codd [4] and others, in four areas. The first is the use of selector names to remove order dependencies from the columns of a relation. This use of selector names enables us to define a more general class of operations, which include the normal relational operations of union, equi-join etc., as special cases. Thirdly we introduce relations represented algorithmically as well as by a stored set of tuples. Such computed relations cannot always be effectively realised as a finite set of tuples. Finally we consider relational expressions as algorithmic representations of relations and characterize their effectiveness.


title: On the Complexity of LR(k) Testing

authors:
Harry B. Hunt III
Thomas G. Szymanski
Jeffrey D. Ullman

abstract: In this paper we derive upper bounds on the complexity of LR(k) testing both when k is considered to be a fixed integer and also when k is considered to be a parameter of the problem. In the latter case, we show that the lower bounds on the running time of such algorithms depend very strongly on the representation chosen for k. Thus LR(k) testing is NP-complete when k is expressed in unary and complete for nondeterministic exponential time when k is expressed in binary.These results carry over to many other parameterized classes of grammars, such as the LL(k), strong LL(k), SLR(k), LC(k), strong LC(k), BRC(l,k), BC(l,k) and extended precedence (l,k) grammars.


title: On the Complexity of the Circularity Test for Attribute Grammars

authors:
Mehdi Jazayeri
William F. Ogden
William C. Rounds

abstract: It is shown that both the upper and the lower bounds on the time complexity of the circularity test for Knuth's attribute grammars are exponential functions of the size of the grammar description. This result implies the "intractability" of the circularity test in the sense that the implementation of a general algorithm is not feasible. Another significance of this result is that this is one of the first problems actually arising in practice which has been proven to be of exponential time complexity.


title: Even Simple Programs are Hard to Analyze

authors:
Neil D. Jones
Steven S. Muchnick

abstract: It has long been known that most questions of interest about the behavior of programs are recursively undecidable. These questions include whether a program will halt, whether two programs are equivalent, whether one is an optimized form of another, and so on. On the other hand, it is possible to make some or all of these questions decidable by suitably restricting the computational ability of the programming language under consideration. The Loop language of Meyer and Ritchie [MR], for example, has a decidable halting problem, but undecidable equivalence. Restricting the computational ability still further, virtually all of these questions are decidable for finite automata and generalized sequential machines (except that Griffiths [Gri] has shown equivalence undecidable for nondeterministic gsms).A natural question to ask is how hard it is to solve these problems for programming languages for which they are decidable, and it is with this area that we are concerned in this paper. In particular we describe a programming language modeled on current higher-level languages which has exactly the computational power of deterministic finite state transducers with final states, and analyze the space and time required to decide various questions of programming interest about the language. We find that questions about halting, equivalence, and optimization are already intractable for this very simple language. We also study extensions to the language such as simple arithmetic capabilities, arrays, and recursive subroutines with both call-by-value and call-by-name parameter passing mechanisms, some of which extend the capabilities of the language and/or increase the complexity of its decidable problems. In one case, that of recursion with call-by-name, the previously decidable questions are seen to become undecidable.


title: Node Listings Applied to Data Flow Analysis

abstract: A new approach to global program data flow analysis which constructs a for the control flow graph is discussed and a simple algorithm which uses a node listing to determine the live variables in a program is presented. This algorithm combined with a fast node listing constructor due to Aho and Ullman has produced an 0(n log n) algorithm for live analysis. The utility of the node-listing method is demonstrated by an examination of the class of graphs for which short listings exist. This class is quite similar to the class of graphs for understandable programs.


title: A Description of Path Expressions by Petri Nets

authors:
Peter E. Lauer
Roy H. Campbell

abstract: Petri nets are used to define a path and process notation which is more general in its ability to express synchronization than previous path notations. The Petri net classes corresponding to the path notation prove to be interesting in their own right and have demonstrable properties such as liveness and safeness.


title: Program Schemas with Concurrency: Execution Time and Hangups

abstract: A class of program schemas with concurrency is defined as a natural extension of the standard notion of sequential flow-chart-like schemas. The question is considered as to whether such a program schema may reach a premature termination (or "hangup") for some interpretation. It is shown that in general this question is undecidable; however, it is shown to be decidable for the class of free program schemas. And an algorithm for testing this property is presented with an upper time bound that grows linearly with the size of the schema.Several structural properties are shown to be equivalent to the hangup-free conditon for free schemas. And we give a method for computing the expected execution time of a program schema if the expected frequencies of choices at the branch points are known.


title: A Mathematical Approach to Language Design

abstract: A framework for validating surface properties of programming language constructs, composed of proof rules (akin to those of Hoare) and supporting hypotheses, is constructed using the mathematical semantics of Scott and Strachey. The following approach to language design is then considered: the constructs of a language should have surface properties which 1) need few hypotheses other than assumed surface properties; and 2) have proofs consisting, as far as possible, of trivial fixpoint and structural inductions.


title: Reduction: A New Method of Proving Properties of Systems of Processes

abstract: When proving that a system of processes has a given property it is often convenient to assume that a routine is uninterruptible, i.e. that the routine cannot be interleaved with the rest of the system. Here sufficient conditions are obtained to show that the assumption that a routine is uninterruptible can be relaxed and still preserve basic properties such as halting and determinacy. Thus correctness proofs of a system of processes can often be greatly simplified. This technique - called reduction - is viewed as the replacement of an interruptible routine by an uninterruptible one.


title: Computer Assisted Application Definition

abstract: This paper describes a system being developed to bridge the gap between an application program and a user inexperienced in the ways of computers. The user explores the characteristics of the available programs by a natural language dialogue with the system. The dialogue is supported by a knowledge base covering both the program semantics and the application domain. This paper addresses the problems of representation and inference involved in this approach and describes our solution for them.


title: Programming Languages, Natural Languages, and Mathematics

abstract: Some social aspects of programming are illuminated through analogies with similar aspects of mathematics and natural languages. The split between pure and applied mathematics is found similarly in programming. The development of natural languages toward flexionless, word-order based language types speaks for programming language design based on general, abstract constructs. By analogy with incidents of the history of artificial, auxiliary languages it is suggested that Fortran and Cobol will remain dominant for a long time to come. The most promising avenues for further work of wide influence is seen to be high quality program literature (i.e. programs) of general utility and studies of questions related to program style.


title: Automatic Data Structure Choice in a Language of Very High Level

abstract: SETL is a set-theoretically oriented language of very high level whose repertoire of semantic objects includes finite sets, ordered n-tuples, and sets of ordered n-tuples useable as mappings. This paper sets forth techniques for the logical analysis and optimization of SETL programs. The techniques described allow relations of inclusion and membership to be established, the domains and ranges of (tabulated) mappings to be estimated from above and below, and the singlevaluedness of (tabulated) mappings to be proved. Once facts of this kind have been established, automatic choice of data structures becomes possible. The methods employed are based upon, and extend, known techniques of data-flow analysis.


title: Modes, Values, and Expressions

abstract: NO ABSTRACT SUPPLIED


title: An Algebraic Model for String Patterns

abstract: Article Free Access Share on An algebraic model for string patterns Author: Glenn F. Stewart I.P. Sharp Associates Limited, Toronto, Ontario, Canada I.P. Sharp Associates Limited, Toronto, Ontario, CanadaView Profile Authors Info & Claims POPL '75: Proceedings of the 2nd ACM SIGACT-SIGPLAN symposium on Principles of programming languagesJanuary 1975 Pages 167–184https://doi.org/10.1145/512976.512994Published:01 January 1975Publication History 8citation252DownloadsMetricsTotal Citations8Total Downloads252Last 12 Months11Last 6 weeks3 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


title: New Control Structures to Aid Gotolessness

abstract: This paper contains a suggestion for a calculus for constructing 'flowchartable' algorithms. The calculus is a generalization of an Algol-like calculus, and hence maintains some discipline over the algorithms constructible with it.The essence of the great 'go to' debate seems to be that the use of the 'go to' device allows the construction of 'spaghetti-like' algorithms which are difficult to control intellectually, and hence that only more restrictive, special-purpose control structures (which are presumably well thought out) should be used. Another way of saying this, perhaps, is that the 'go to' device is the most primitive (and hence most general) possible control structure, and though implementations of any control structure will ultimately have to be done using it, a programmer should no more be content using a 'go to' than if he were forced to use bit strings for data types. He should be demanding higher-level control structures. To some extent, of course, he has them; but, in discussing the 'go to' debate, the conclusion arrived at by Knuth (1), for instance, is that more powerful control structures than are freely available at present are needed to enable programmers to express their algorithms. He mentions a suggestion by Zahn (2) for strengthening the set of available control structures, but shows that he still needs to resort to the dreaded 'go to' device. (He confesses a sinful urge to jump into the middle of Zahn's loops.) The implication is that even with Zahn's suggestions there is a need for more control structures. We concur with this view, and present here a suggestion for making more such structures available. We invite discussion as to whether the results are profitable for programming language design.The lack of well-developed control structures is manifested, incidentally, not only in the dearth of 'public' control structures (i.e. made freely available to all users), but also in the lack of facilities for creating 'private' ones (analogously to the notion of 'subroutines' or user-defined data types). These deficiencies are not all that surprising since control structures are, in a sense, devices at a third level of sophistication: data (being the first level) is acted upon by programs (being the second level) to produce other data; and programs are acted upon by control structures to produce other programs. But the time has perhaps come to pay some more attention to control structures.


title: Code Generation for Expressions with Common Subexpressions

authors:
Alfred V. Aho
Stephen C. Johnson
Jeffrey D. Ullman

abstract: Easy as the task may seem, many compilers generate rather inefficient code. Some of the difficulty of generating good code may arise from the lack of realistic models for programming language and machine semantics. In this paper we show that the computational complexity of generating efficient code in realistic situations may also be a major cause of difficulty in the design of good compilers.


title: An Algorithm for Structuring Programs

abstract: Structured programming emphasizes programming language constructs such as while loops, until loops, and if then else statements. Properly used, these constructs make occurrences of loops and branching of control obvious. They are preferable to goto statements, which tend to obscure the flow of control [DDH,DIJ]. This paper describes an algorithm which transforms a flowgraph into a program written using repeat (do forever) and if then else statements. The goal of the algorithm is to produce readable programs, rather than to avoid the use of goto statements entirely. goto statements are generated when there is no better way to describe the flow of control.


title: Primitive Recursive Program Transformations

authors:
Robert S. Boyer
J Strother Moore
Robert E. Shostak

abstract: We describe how to transform certain flowchart programs into equivalent explicit primitive recursive programs. The input/output correctness conditions for the transformed programs are more amenable to proof than the verification conditions for the corresponding flowchart programs. In particular, the transformed correctness conditions can often be verified automatically by the theorem prover developed by Boyer and Moore [1].


title: Procedure Referencing Environments in SL5

authors:
Dianne E. Britton
Frederick C. Druseikis
Ralph E. Griswold
David R. Hanson
Richard A. Holmes

abstract: SL5 is a programming language developed for experimental work in generalized pattern matching and high-level data structuring and access mechanisms. This paper describes the procedure mechanism and the conventions for the interpretation of identifiers in SL5. Procedure invocation in SL5 is decomposed into the separate source-language operations of context creation, argument binding and procedure activation, and allows SL5 procedures to be used as recursive functions or coroutines. This decomposition has led to rules for scoping and for the interpretation of identifiers that are different from those found in other programming languages. Several examples of SL5 procedures are given, including a scanner based on the coroutine model of pattern matching.


title: Induction Variables in Very High Level Languages

authors:
Amelia C. Fong
Jeffrey D. Ullman

abstract: We explore the notion of an induction variable in the context of a set-theoretic programming langugage. An appropriate definition, we believe, involves both the necessity that changes in the variable around a loop be easily computable and that they be small. We attempt to justify these requirements and show why they are independent assumptions. Next the question of what operators on sets play the role of +, − and * for arithmetic languages is explored, and several theorems allowing us recursively to detect induction variables in a loop are given. It is shown that most of the usual set operations do fit nicely into the theory and help form induction variables. The reason most variables fail to be induction variables concerns the structure of control flow, more than it does the operators applied.


title: PLAN2D - Syntactic Analysis of Precedence Graph Grammars

abstract: The syntactical analysis of pictures derived by a context-free graph-grammar is a rather complicated algorithm. Analogously to the development for Chomsky-grammars ten years ago we define the precedence-graph-grammars as a subclass of the context-free graph-grammars allowing for easier parsing algorithms. By table-lookup we can decide locally if an edge or a node is part of a handle and if it isn't in which direction to proceed to reach one.


title: Test Data as an Aid in Proving Program Correctness

abstract: Proofs of program correctness tend to be long and tedious whereas testing, though useful in detecting errors, usually does not guarantee correctness. This paper introduces a technique whereby test data can be used in proving program correctness. In addition to simplifying certification of correctness, this method simplifies the process of providing specifications for a program. The applicability of this technique to procedures, recursive programs, and modular programs is demonstrated.


title: Verifying Formal Specifications of Synchronous Processes

authors:
Patricia P. Griffiths
Charles J. Prenner

abstract: SYNVER is an automatic programming system for the synthesis of solutions to problems of synchronization among concurrent processes from specifications written in a high level assertion language (SAL). The correctness of the solutions constructed by SYNVER follows from the soundness of the synthesizer itself and from a verification phase which is applied to the specifications. This verification phase is the main topic of this paper. To provide context for the verification the paper includes a discussion of synchronization problems and a brief overview of both the SYNVER system and the SAL specification language. A formal definition of the correctness of a SAL specification is then presented along with algorithms which may be used to determine if a given specification is correct.


title: A Lazy Evaluator

authors:
Peter Henderson
James H. Morris Jr.

abstract: A different way to execute pure LISP programs is presented. It delays the evaluation of parameters and list structures without ever having to perform more evaluation steps than the usual method. Although the central idea can be found in earlier work this paper is of interest since it treats a rather well-known language and works out an algorithm which avoids full substitution. A partial correctness proof using Scott-Strachey semantics is sketched in a later section.


title: A Complexity Theory of Grammar Problems

abstract: The close relationship between programming language syntax, context-free grammars (abbreviated cfgs), parsing, and compiling is well-known and is extensively discussed in [1]. Unfortunately, many of the problems about programming languages, one might wish to solve, are equivalent to undecidable grammar problems. Two especially important such problems are


title: Binding Time Optimization in Programming Languages: Some Thoughts Toward the Design of an Ideal Language

abstract: A new approach to the design of a programming language and its processor is proposed and some of the techniques necessary to realize the design are investigated. The language would have a precisely specified syntax and semantics, with both designed to provide the programmer maximal expressive power and to be as easily understood as possible. The semantics would be based on extremely late binding times, which provide great power to the programmer and are consistent with ease of understanding of the execution process. It would be the responsibility of the processor to implement each program in the most efficient manner consistent with its being correctly executed. Implications of this design philosophy and some of the techniques to be used are discussed in greater detail, focusing particularly on data types and storage allocation.