相关论文: Vector Clocks in Coq: An Experience Report

Software certification aims at proving the correctness of programs but in many cases, the use of external libraries allows only a conditional proof: it depends on the assumption that the libraries meet their specifications. In particular, a…

Capitalizing on previous encodings and formal developments about nominal calculi and type systems, we propose a weak Higher-Order Abstract Syntax formalization of the type language of pure System F<: within Coq, a proof assistant based on…

We describe an application of Prolog: a type checking tool for the Q functional language. Q is a terse vector processing language, a descendant of APL, which is getting more and more popular, especially in financial applications. Q is a…

In this paper we consider the problem of certified static checking of module-like constructs of programming languages. We argue that there are algorithms and properties related to modules that can be defined and proven in an abstract way.…

We report on using an agentic coding assistant (Claude Code, powered by Claude Opus 4.6) to mechanize a substantial Rocq correctness proof from scratch, with human guidance but without human proof writing. The proof establishes semantic…

Large language models (LLMs) can potentially help with verification using proof assistants by automating proofs. However, it is unclear how effective LLMs are in this task. In this paper, we perform a case study based on two mature Rocq…

Zk-SNARKs help scale blockchains with Verifiable Off-chain Computations (VOC). zk-SNARK DSL toolkits are key when designing arithmetic circuits but fall short of automating the subsequent proof-generation step in an automated manner. We…

In this paper, we propose Proq, a runtime assertion scheme for testing and debugging quantum programs on a quantum computer. The predicates in Proq are represented by projections (or equivalently, closed subspaces of the state space),…

We exploit (co)inductive specifications and proofs to approach the evaluation of low-level programs for the Unlimited Register Machine (URM) within the Coq system, a proof assistant based on the Calculus of (Co)Inductive Constructions type…

This notes explains how standard algorithms that construct sorting networks have been formalised and proved correct in the Coq proof assistant using the SSReflect extension.

What provides the highest level of assurance for correctness of execution within a programming language? One answer, and our solution in particular, to this problem is to provide a formalization for, if it exists, the denotational semantics…

Vector architectures lack tools for research. Consider the gem5 simulator, which is possibly the leading platform for computer-system architecture research. Unfortunately, gem5 does not have an available distribution that includes a…

PyLog is a minimal experimental proof assistant based on linearised natural deduction for intuitionistic and classical first-order logic extended with a comprehension operator. PyLog is interesting as a tool to be used in conjunction with…

We report the results of the first experiments with learning proof dependencies from the formalizations done with the Coq system. We explain the process of obtaining the dependencies from the Coq proofs, the characterization of formulas…

We describe jsCcoq, a new platform and user environment for the Coq interactive proof assistant. The jsCoq system targets the HTML5-ECMAScript 2015 specification, and it is typically run inside a standards-compliant browser, without the…

In this report we describe a tool framework for certifying properties of PLCs: CERTPLC. CERTPLC can handle PLC descriptions provided in the Sequential Function Chart (SFC) language of the IEC 61131-3 standard. It provides routines to…

We consider the task of analyzing message-passing programs by observing their run-time behavior. We introduce a purely library-based instrumentation method to trace communication events during execution. A model of the dependencies among…

Time is an important feature in many applications involving events that occur synchronously and/or asynchronously. To effectively consume time information, recent studies have focused on designing new architectures. In this paper, we take…

LLM-based code assistants are becoming increasingly popular among developers. These tools help developers improve their coding efficiency and reduce errors by providing real-time suggestions based on the developer's codebase. While…

Formally reasoning about functional programs is supposed to be straightforward and elegant, however, it is not typically done as a matter of course. Reasoning in a proof assistant requires "reimplementing" the code in those tools, which is…