Journal articles: 'Coq (assistant de preuve)'

1

Gäher, Lennard, Michael Sammler, Ralf Jung, Robbert Krebbers, and Derek Dreyer. "RefinedRust: A Type System for High-Assurance Verification of Rust Programs." Proceedings of the ACM on Programming Languages 8, PLDI (June 20, 2024): 1115–39. http://dx.doi.org/10.1145/3656422.

Full text

Abstract:

Rust is a modern systems programming language whose ownership-based type system statically guarantees memory safety, making it particularly well-suited to the domain of safety-critical systems. In recent years, a wellspring of automated deductive verification tools have emerged for establishing functional correctness of Rust code. However, none of the previous tools produce foundational proofs (machine-checkable in a general-purpose proof assistant), and all of them are restricted to the safe fragment of Rust. This is a problem because the vast majority of Rust programs make use of unsafe code at critical points, such as in the implementation of widely-used APIs. We propose RefinedRust, a refinement type system—proven sound in the Coq proof assistant—with the goal of establishing foundational semi-automated functional correctness verification of both safe and unsafe Rust code. We have developed a prototype verification tool implementing RefinedRust. Our tool translates Rust code (with user annotations) into a model of Rust embedded in Coq, and then checks its adherence to the RefinedRust type system using separation logic automation in Coq. All proofs generated by RefinedRust are checked by the Coq proof assistant, so the automation and type system do not have to be trusted. We evaluate the effectiveness of RefinedRust by verifying a variant of Rust’s Vec implementation that involves intricate reasoning about unsafe pointer-manipulating code.

APA, Harvard, Vancouver, ISO, and other styles

2

Zhou, Litao, Jianxing Qin, Qinshi Wang, Andrew W. Appel, and Qinxiang Cao. "VST-A: A Foundationally Sound Annotation Verifier." Proceedings of the ACM on Programming Languages 8, POPL (January 5, 2024): 2069–98. http://dx.doi.org/10.1145/3632911.

Full text

Abstract:

Program verifiers for imperative languages such as C may be annotation-based, in which assertions and invariants are put into source files and then checked, or tactic-based, where proof scripts separate from programs are interactively developed in a proof assistant such as Coq. Annotation verifiers have been more automated and convenient, but some interactive verifiers have richer assertion languages and formal proofs of soundness. We present VST-A, an annotation verifier that uses the rich assertion language of VST, leverages the formal soundness proof of VST, but allows users to describe functional correctness proofs intuitively by inserting assertions. VST-A analyzes control flow graphs, decomposes every C function into control flow paths between assertions, and reduces program verification problems into corresponding straightline Hoare triples. Compared to existing foundational program verification tools like VST and Iris, in VST-A such decompositions and reductions can nonstructural, which makes VST-A more flexible to use. VST-A's decomposition and reduction is defined in Coq, proved sound in Coq, and computed call-by-value in Coq. The soundness proof for reduction is totally logical, independent of the complicated semantic model (and soundness proof) of VST's Hoare triple. Because of the rich assertion language, not all reduced proof goals can be automatically checked, but the system allows users to prove residual proof goals using the full power of the Coq proof assistant.

APA, Harvard, Vancouver, ISO, and other styles

3

VOEVODSKY, VLADIMIR. "An experimental library of formalized Mathematics based on the univalent foundations." Mathematical Structures in Computer Science 25, no. 5 (January 20, 2015): 1278–94. http://dx.doi.org/10.1017/s0960129514000577.

Full text

Abstract:

This is a short overview of an experimental library of Mathematics formalized in the Coq proof assistant using the univalent interpretation of the underlying type theory of Coq. I started to work on this library in February 2010 in order to gain experience with formalization of Mathematics in a constructive type theory based on the intuition gained from the univalent models (see Kapulkin et al. 2012).

APA, Harvard, Vancouver, ISO, and other styles

4

MAHBOUBI, ASSIA. "Implementing the cylindrical algebraic decomposition within the Coq system." Mathematical Structures in Computer Science 17, no. 1 (February 2007): 99–127. http://dx.doi.org/10.1017/s096012950600586x.

Full text

Abstract:

The Coq system is a Curry–Howard based proof assistant. Therefore, it contains a full functional, strongly typed programming language, which can be used to enhance the system with powerful automation tools through the implementation of reflexive tactics. We present the implementation of a cylindrical algebraic decomposition algorithm within the Coq system, whose certification leads to a proof producing decision procedure for the first-order theory of real numbers.

APA, Harvard, Vancouver, ISO, and other styles

5

Zúñiga, Angel, and Gemma Bel-Enguix. "Coinductive Natural Semantics for Compiler Verification in Coq." Mathematics 8, no. 9 (September 12, 2020): 1573. http://dx.doi.org/10.3390/math8091573.

Full text

Abstract:

(Coinductive) natural semantics is presented as a unifying framework for the verification of total correctness of compilers in Coq (with the feature that a verified compiler can be obtained). In this way, we have a simple, easy, and intuitive framework; to carry out the verification of a compiler, using a proof assistant in which both cases are considered: terminating and non-terminating computations (total correctness).

APA, Harvard, Vancouver, ISO, and other styles

6

Wang, Qian, Xiaoyu Song, Ming Gu, and Jiaguang Sun. "Functional Verification of High Performance Adders in COQ." Journal of Applied Mathematics 2014 (2014): 1–9. http://dx.doi.org/10.1155/2014/197252.

Full text

Abstract:

Addition arithmetic design plays a crucial role in high performance digital systems. The paper proposes a systematic method to formalize and verify adders in a formal proof assistant COQ. The proposed approach succeeds in formalizing the gate-level implementations and verifying the functional correctness of the most important adders of interest in industry, in a faithful, scalable, and modularized way. The methodology can be extended to other adder architectures as well.

APA, Harvard, Vancouver, ISO, and other styles

7

Forster, Yannick, Dominik Kirst, and Dominik Wehr. "Completeness theorems for first-order logic analysed in constructive type theory." Journal of Logic and Computation 31, no. 1 (January 2021): 112–51. http://dx.doi.org/10.1093/logcom/exaa073.

Full text

Abstract:

Abstract We study various formulations of the completeness of first-order logic phrased in constructive type theory and mechanised in the Coq proof assistant. Specifically, we examine the completeness of variants of classical and intuitionistic natural deduction and sequent calculi with respect to model-theoretic, algebraic, and game-theoretic semantics. As completeness with respect to the standard model-theoretic semantics à la Tarski and Kripke is not readily constructive, we analyse connections of completeness theorems to Markov’s Principle and Weak Kőnig’s Lemma and discuss non-standard semantics admitting assumption-free completeness. We contribute a reusable Coq library for first-order logic containing all results covered in this paper.

APA, Harvard, Vancouver, ISO, and other styles

8

PELAYO, ÁLVARO, VLADIMIR VOEVODSKY, and MICHAEL A. WARREN. "A univalent formalization of the p-adic numbers." Mathematical Structures in Computer Science 25, no. 5 (February 13, 2015): 1147–71. http://dx.doi.org/10.1017/s0960129514000541.

Full text

Abstract:

The goal of this paper is to report on a formalization of the p-adic numbers in the setting of the second author's univalent foundations program. This formalization, which has been verified in the Coq proof assistant, provides an approach to the p-adic numbers in constructive algebra and analysis.

APA, Harvard, Vancouver, ISO, and other styles

9

Sacchini, Jorge Luis. "Towards a New Termination Checker for the Coq Proof Assistant." Qatar Foundation Annual Research Forum Proceedings, no. 2011 (November 2011): CSP23. http://dx.doi.org/10.5339/qfarf.2011.csp23.

Full text

APA, Harvard, Vancouver, ISO, and other styles

10

Huet, Gérard. "Residual theory in λ-calculus: a formal development." Journal of Functional Programming 4, no. 3 (July 1994): 371–94. http://dx.doi.org/10.1017/s0956796800001106.

Full text

Abstract:

AbstractWe present the complete development, in Gallina, of the residual theory of β-reduction in pure λ-calculus. The main result is the Prism Theorem, and its corollary Lévy's Cube Lemma, a strong form of the parallel-moves lemma, itself a key step towards the confluence theorem and its usual corollaries (Church-Rosser, uniqueness of normal forms). Gallina is the specification language of the Coq Proof Assistant (Dowek et al., 1991; Huet 1992b). It is a specific concrete syntax for its abstract framework, the Calculus of Inductive Constructions (Paulin-Mohring, 1993). It may be thought of as a smooth mixture of higher-order predicate calculus with recursive definitions, inductively defined data types and inductive predicate definitions reminiscent of logic programming. The development presented here was fully checked in the current distribution version Coq V5.8. We just state the lemmas in the order in which they are proved, omitting the proof justifications. The full transcript is available as a standard library in the distribution of Coq.

APA, Harvard, Vancouver, ISO, and other styles

11

AVIGAD, JEREMY, KRZYSZTOF KAPULKIN, and PETER LEFANU LUMSDAINE. "Homotopy limits in type theory." Mathematical Structures in Computer Science 25, no. 5 (January 19, 2015): 1040–70. http://dx.doi.org/10.1017/s0960129514000498.

Full text

Abstract:

Working in homotopy type theory, we provide a systematic study of homotopy limits of diagrams over graphs, formalized in the Coq proof assistant. We discuss some of the challenges posed by this approach to the formalizing homotopy-theoretic material. We also compare our constructions with the more classical approach to homotopy limits via fibration categories.

APA, Harvard, Vancouver, ISO, and other styles

12

Ekici, Burak. "A Sound Definitional Interpreter for a Simply Typed Functional Language." Axioms 12, no. 1 (December 30, 2022): 43. http://dx.doi.org/10.3390/axioms12010043.

Full text

Abstract:

In this paper, we develop, in the proof assistant Coq, a definitional interpreter and a type-checker for a simply typed functional language, and formally prove that the mentioned type-checker is sound with respect to the definitional interpreter via progress and preservation. To represent binders, we embark on the choice of “concrete syntax” in which parameters are just names (or strings).

APA, Harvard, Vancouver, ISO, and other styles

13

Rouquet, Karine. "David Lynch." Revista Estado da Arte 2, no. 1 (June 15, 2021): 1–15. http://dx.doi.org/10.14393/eda-v2-n1-2021-59834.

Full text

Abstract:

Ce petit film, au-delà de l’héritage revendiqué du surréalisme, utilise des procédés comiques et fantastiques hybrides (création d’une chimère, narration disruptive, dialogues abusant du coq-à-l’âne et tournant à la fatrasie) qui relèvent de l’inversion carnavalesque décrite par Michaël Bakhtine et plus particulièrement de la Sottie, pièce satyrique en vers que l’on représentait au moment du carnaval. La référence aux Absurda de Érasme en serait la preuve. Dans cette parade bouffonne, David Lynch en Maître-Sot ou Maître es Folie s’amuse à court-circuiter les codes du film noir de la narration, comme de as propre filmographie, créant une esthétique turbulente propre à défier la plateforme disruptive sur laquelle il fait son entrée.

APA, Harvard, Vancouver, ISO, and other styles

14

Gruetter, Samuel, Viktor Fukala, and Adam Chlipala. "Live Verification in an Interactive Proof Assistant." Proceedings of the ACM on Programming Languages 8, PLDI (June 20, 2024): 1535–58. http://dx.doi.org/10.1145/3656439.

Full text

Abstract:

We present a prototype for a tool that enables programmers to verify their code as they write it in real-time. After each line of code that the programmer writes, the tool tells the programmer whether it was able to prove absence of undefined behavior so far, and it displays a concise representation of the symbolic state of the program right after the added line. The user can then either write the next line of code, or if needed or desired, write a specially marked comment that provides hints on how to solve side conditions or on how to represent the symbolic state more nicely. Once the programmer has finished writing the program, it is already verified with a mathematical correctness proof. Other tools providing real-time feedback already exist, but ours is the first one that only relies on a small trusted proof checker and that provides a concise summary of the symbolic state at the point in the program currently being edited, as opposed to only indicating whether user-stated assertions or postconditions hold. Program verification requires loop invariants, which are hard to find and tedious to spell out. We explore a middle ground in the design space between the two extremes of requiring users to spell out loop invariants manually and attempting to infer loop invariants automatically: Since a loop invariant often looks quite similar to the symbolic state right before the loop, our tool asks the user to express the desired loop invariant as a diff from the symbolic state before the loop, which has the potential to lead to shorter, more maintainable proofs. We prototyped our technique in the interactive proof assistant Coq, so our framework creates machine-checked proofs that the developed functions satisfy their specifications when executed according to the formal semantics of the source language. Using a verified compiler proven against the same source-language semantics, we can ensure that the behavior of the compiled program matches the program's behavior as represented by the framework during the proof. Additionally, since our polyglot source files can be viewed as Coq or C files at the same time, users willing to accept a larger trusted code base can compile them with GCC.

APA, Harvard, Vancouver, ISO, and other styles

15

Forster, Yannick, Matthieu Sozeau, and Nicolas Tabareau. "Verified Extraction from Coq to OCaml." Proceedings of the ACM on Programming Languages 8, PLDI (June 20, 2024): 52–75. http://dx.doi.org/10.1145/3656379.

Full text

Abstract:

One of the central claims of fame of the Coq proof assistant is extraction, i.e. the ability to obtain efficient programs in industrial programming languages such as OCaml, Haskell, or Scheme from programs written in Coq’s expressive dependent type theory. Extraction is of great practical usefulness, used crucially e.g. in the CompCert project. However, for such executables obtained by extraction, the extraction process is part of the trusted code base (TCB), as are Coq’s kernel and the compiler used to compile the extracted code. The extraction process contains intricate semantic transformation of programs that rely on subtle operational features of both the source and target language. Its code has also evolved since the last theoretical exposition in the seminal PhD thesis of Pierre Letouzey. Furthermore, while the exact correctness statements for the execution of extracted code are described clearly in academic literature, the interoperability with unverified code has never been investigated formally, and yet is used in virtually every project relying on extraction. In this paper, we describe the development of a novel extraction pipeline from Coq to OCaml, implemented and verified in Coq itself, with a clear correctness theorem and guarantees for safe interoperability. We build our work on the MetaCoq project, which aims at decreasing the TCB of Coq’s kernel by re-implementing it in Coq itself and proving it correct w.r.t. a formal specification of Coq’s type theory in Coq. Since OCaml does not have a formal specification, we make use of the project specifying the semantics of the intermediate language of the OCaml compiler. Our work fills some gaps in the literature and highlights important differences between the operational semantics of Coq programs and their extraction. In particular, we focus on the guarantees that can be provided for interoperability with unverified code, and prove that extracted programs of first-order data type are correct and can safely interoperate, whereas for higher-order programs already simple interoperations can lead to incorrect behaviour and even outright segfaults.

APA, Harvard, Vancouver, ISO, and other styles

16

Michelland, Sébastien, Yannick Zakowski, and Laure Gonnord. "Abstract Interpreters: A Monadic Approach to Modular Verification." Proceedings of the ACM on Programming Languages 8, ICFP (August 15, 2024): 602–29. http://dx.doi.org/10.1145/3674646.

Full text

Abstract:

We argue that monadic interpreters built as layers of interpretations stacked atop the free monad constitute a promising way to implement and verify abstract interpreters in dependently-typed theories such as the one underlying the Coq proof assistant. The approach enables modular proofs of soundness of the resulting interpreters. We provide generic abstract control flow combinators proven correct once and for all against their concrete counterpart. We demonstrate how to relate concrete handlers implementing effects to abstract variants of these handlers, essentially capturing the traditional soundness of transfer functions in the context of monadic interpreters. Finally, we provide generic results to lift soundness statements via the interpretation of stateful and failure effects. We formalize all the aforementioned combinators and theories in Coq, and demonstrate their benefits by implementing and proving correct two illustrative abstract interpreters for a structured imperative language and a toy assembly.

APA, Harvard, Vancouver, ISO, and other styles

17

Affeldt, Reynald, Naoki Kobayashi, and Akinori Yonezawa. "Verification of Concurrent Programs Using the Coq Proof Assistant: A Case Study." IPSJ Digital Courier 1 (2005): 117–27. http://dx.doi.org/10.2197/ipsjdc.1.117.

Full text

APA, Harvard, Vancouver, ISO, and other styles

18

Böhne, Sebastian, and Christoph Kreitz. "Learning how to Prove: From the Coq Proof Assistant to Textbook Style." Electronic Proceedings in Theoretical Computer Science 267 (March 2, 2018): 1–18. http://dx.doi.org/10.4204/eptcs.267.1.

Full text

APA, Harvard, Vancouver, ISO, and other styles

19

Cohen, Joshua M., and Philip Johnson-Freyd. "A Formalization of Core Why3 in Coq." Proceedings of the ACM on Programming Languages 8, POPL (January 5, 2024): 1789–818. http://dx.doi.org/10.1145/3632902.

Full text

Abstract:

Intermediate verification languages like Why3 and Boogie have made it much easier to build program verifiers, transforming the process into a logic compilation problem rather than a proof automation one. Why3 in particular implements a rich logic for program specification with polymorphism, algebraic data types, recursive functions and predicates, and inductive predicates; it translates this logic to over a dozen solvers and proof assistants. Accordingly, it serves as a backend for many tools, including Frama-C, EasyCrypt, and GNATProve for Ada SPARK. But how can we be sure that these tools are correct? The alternate foundational approach, taken by tools like VST and CakeML, provides strong guarantees by implementing the entire toolchain in a proof assistant, but these tools are harder to build and cannot directly take advantage of SMT solver automation. As a first step toward enabling automated tools with similar foundational guarantees, we give a formal semantics in Coq for the logic fragment of Why3. We show that our semantics are useful by giving a correct-by-construction natural deduction proof system for this logic, using this proof system to verify parts of Why3's standard library, and proving sound two of Why3's transformations used to convert terms and formulas into the simpler logics supported by the backend solvers.

APA, Harvard, Vancouver, ISO, and other styles

20

Fu, Yaoshun, and Wensheng Yu. "Formalization of the Equivalence among Completeness Theorems of Real Number in Coq." Mathematics 9, no. 1 (December 25, 2020): 38. http://dx.doi.org/10.3390/math9010038.

Full text

Abstract:

The formalization of mathematics based on theorem prover becomes increasingly important in mathematics and computer science, and, particularly, formalizing fundamental mathematical theories becomes especially essential. In this paper, we describe the formalization in Coq of eight very representative completeness theorems of real numbers. These theorems include the Dedekind fundamental theorem, Supremum theorem, Monotone convergence theorem, Nested interval theorem, Finite cover theorem, Accumulation point theorem, Sequential compactness theorem, and Cauchy completeness theorem. We formalize the real number theory strictly following Landau’s Foundations of Analysis where the Dedekind fundamental theorem can be proved. We extend this system and complete the related notions and properties for finiteness and sequence. We prove these theorems in turn from Dedekind fundamental theorem, and finally prove the Dedekind fundamental theorem by the Cauchy completeness theorem. The full details of formal proof are checked by the proof assistant Coq, which embodies the characteristics of reliability and interactivity. This work can lay the foundation for many applications, especially in calculus and topology.

APA, Harvard, Vancouver, ISO, and other styles

21

Danvy, Olivier. "Getting There and Back Again." Fundamenta Informaticae 185, no. 2 (May 2, 2022): 115–83. http://dx.doi.org/10.3233/fi-222106.

Full text

Abstract:

“There and Back Again” (TABA) is a programming pattern where the recursive calls traverse one data structure and the subsequent returns traverse another. This article presents new TABA examples, refines existing ones, and formalizes both their control flow and their data flow using the Coq Proof Assistant. Each formalization mechanizes a pen-and-paper proof, thus making it easier to “get” TABA. In addition, this article identifies and illustrates a tail-recursive variant of TABA, There and Forth Again (TAFA) that does not come back but goes forth instead with more tail calls.

APA, Harvard, Vancouver, ISO, and other styles

22

BONIFATI, ANGELA, STEFANIA DUMBRAVA, and EMILIO JESÚS GALLEGO ARIAS. "Certified Graph View Maintenance with Regular Datalog." Theory and Practice of Logic Programming 18, no. 3-4 (July 2018): 372–89. http://dx.doi.org/10.1017/s1471068418000224.

Full text

Abstract:

AbstractWe employ the Coq proof assistant to develop a mechanically-certified framework for evaluating graph queries and incrementally maintaining materialized graph instances, also called views. The language we use for defining queries and views is Regular Datalog (RD) – a notable fragment of non-recursive Datalog that can express complex navigational queries, with transitive closure as native operator. We first design and encode the theory of RD and then mechanize a RD-specific evaluation algorithm capable of fine-grained, incremental graph view computation, which we prove sound with respect to the declarative RD semantics. By using the Coq extraction mechanism, we test an OCaml version of the verified engine on a set of preliminary benchmarks. Our development is particularly focused on leveraging existing verification and notational techniques to: a) define mechanized properties that can be easily understood by logicians and database researchers and b) attain formal verification with limited effort. Our work is the first step towards a unified, machine-verified, formal framework for dynamic graph query languages and their evaluation engines.

APA, Harvard, Vancouver, ISO, and other styles

23

HIRAI, YOICHI, and KAZUHIKO YAMAMOTO. "Balancing weight-balanced trees." Journal of Functional Programming 21, no. 3 (May 2011): 287–307. http://dx.doi.org/10.1017/s0956796811000104.

Full text

Abstract:

AbstractA weight-balanced tree (WBT) is a binary search tree, whose balance is based on the sizes of the subtrees in each node. Although purely functional implementations on a variant WBT algorithm are widely used in functional programming languages, many existing implementations do not maintain balance after deletion in some cases. The difficulty lies in choosing a valid pair of rotation parameters: one for standard balance and the other for choosing single or double rotation. This paper identifies the exact valid range of the rotation parameters for insertion and deletion in the original WBT algorithm where one and only one integer solution exists. Soundness of the range is proved using a proof assistant Coq. Completeness is proved using effective algorithms generating counterexample trees. For two specific parameter pairs, we also proved in Coq that set operations also maintain balance. Since the difference between the original WBT and the variant WBT is small, it is easy to change the existing buggy implementations based on the variant WBT to the certified original WBT with a rational solution.

APA, Harvard, Vancouver, ISO, and other styles

24

Jin, Ende, Nada Amin, and Yizhou Zhang. "Extensible Metatheory Mechanization via Family Polymorphism." Proceedings of the ACM on Programming Languages 7, PLDI (June 6, 2023): 1608–32. http://dx.doi.org/10.1145/3591286.

Full text

Abstract:

With the growing practice of mechanizing language metatheories, it has become ever more pressing that interactive theorem provers make it easy to write reusable, extensible code and proofs. This paper presents a novel language design geared towards extensible metatheory mechanization in a proof assistant. The new design achieves reuse and extensibility via a form of family polymorphism, an object-oriented idea, that allows code and proofs to be polymorphic to their enclosing families. Our development addresses technical challenges that arise from the underlying language of a proof assistant being simultaneously functional, dependently typed, a logic, and an interactive tool. Our results include (1) a prototypical implementation of the language design as a Coq plugin, (2) a dependent type theory capturing the essence of the language mechanism and its consistency and canonicity results, and (3) case studies showing how the new expressiveness naturally addresses real programming challenges in metatheory mechanization.

APA, Harvard, Vancouver, ISO, and other styles

25

CHLIPALA, ADAM. "Modular development of certified program verifiers with a proof assistant,." Journal of Functional Programming 18, no. 5-6 (August 15, 2008): 599–647. http://dx.doi.org/10.1017/s0956796808006904.

Full text

Abstract:

AbstractWe report on an experience using the Coq proof assistant to develop a program verification tool with a machine-checked proof of full correctness. The verifier is able to prove memory safety of x86 machine code programs compiled from code that uses algebraic datatypes. The tool's soundness theorem is expressed in terms of the bit-level semantics of x86 programs, so its correctness depends on very few assumptions. We take advantage of Coq's support for programming with dependent types and modules in the structure of the development. The approach is based on developing a library of reusable functors for transforming a verifier at one level of abstraction into a verifier at a lower level. Using this library, it is possible to prototype a verifier based on a new type system with a minimal amount of work, while obtaining a very strong soundness theorem about the final product.

APA, Harvard, Vancouver, ISO, and other styles

26

Gladstein, Vladimir, Dmitrii Mikhailovskii, Evgenii Moiseenko, and Anton Trunov. "Mechanized Theory of Event Structures: A Case of Parallel Register Machine." Proceedings of the Institute for System Programming of the RAS 33, no. 3 (2021): 143–54. http://dx.doi.org/10.15514/ispras-2021-33(3)-11.

Full text

Abstract:

The true concurrency models, and in particular event structures, have been introduced in the 1980s as an alternative to operational interleaving semantics of concurrency, and nowadays they are regaining popularity. Event structures represent the causal dependency and conflict between the individual atomic actions of the system directly. This property leads to a more compact and concise representation of semantics. In this work-in-progress report, we present a theory of event structures mechanized in the COQ proof assistant and demonstrate how it can be applied to define certified executable semantics of a simple parallel register machine with shared memory.

APA, Harvard, Vancouver, ISO, and other styles

27

SEWELL, PETER, FRANCESCO ZAPPA NARDELLI, SCOTT OWENS, GILLES PESKINE, THOMAS RIDGE, SUSMIT SARKAR, and ROK STRNIŠA. "Ott: Effective tool support for the working semanticist." Journal of Functional Programming 20, no. 1 (January 2010): 71–122. http://dx.doi.org/10.1017/s0956796809990293.

Full text

Abstract:

AbstractSemantic definitions of full-scale programming languages are rarely given, despite the many potential benefits. Partly this is because the available metalanguages for expressing semantics – usually either for informal mathematics or the formal mathematics of a proof assistant – make it much harder than necessary to work with large definitions. We present a metalanguage specifically designed for this problem, and a tool, Ott, that sanity-checks such definitions and compiles them into proof assistant code for Coq, HOL, and Isabelle/HOL, together with code for production-quality typesetting, and OCaml boilerplate. The main innovations are (1) metalanguage design to make definitions concise, and easy to read and edit; (2) an expressive but intuitive metalanguage for specifying binding structures; and (3) compilation to proof assistant code. This has been tested in substantial case studies, including modular specifications of calculi from the TAPL text, a Lightweight Java with Java JSR 277/294 module system proposals, and a large fragment of OCaml (OCamllight, 310 rules), with mechanised proofs of various soundness results. Our aim with this work is to enable a phase change: making it feasible to work routinely, without heroic effort, with rigorous semantic definitions of realistic languages.

APA, Harvard, Vancouver, ISO, and other styles

28

PAŞCA, IOANA. "Formal proofs for theoretical properties of Newton's method." Mathematical Structures in Computer Science 21, no. 4 (July 1, 2011): 683–714. http://dx.doi.org/10.1017/s0960129511000077.

Full text

Abstract:

We discuss a formal development for the certification of Newton's method. We address several issues encountered in the formal study of numerical algorithms: developing the necessary libraries for our proofs, adapting paper proofs to suit the features of a proof assistant and designing new proofs based on the existing ones to deal with optimisations of the method. We start from Kantorovitch's Theorem, which gives the convergence of Newton's method in the case of a system of equations. To formalise this proof inside the proof assistant Coq, we first need to code the necessary concepts from multivariate analysis. We also prove that rounding at each step in Newton's method still yields a convergent process with an accurate correlation between the precision of the input and that of the result. This proof is based on Kantorovitch's Theorem, but is an original result. An algorithm including rounding is a more accurate model for computations with Newton's method in practice.

APA, Harvard, Vancouver, ISO, and other styles

29

Gopinathan, Kiran, Mayank Keoliya, and Ilya Sergey. "Mostly Automated Proof Repair for Verified Libraries." Proceedings of the ACM on Programming Languages 7, PLDI (June 6, 2023): 25–49. http://dx.doi.org/10.1145/3591221.

Full text

Abstract:

The cost of maintaining formally specified and verified software is widely considered prohibitively high due to the need to constantly keep code and the proofs of its correctness in sync—the problem known as proof repair . One of the main challenges in automated proof repair for evolving code is to infer invariants for a new version of a once verified program that are strong enough to establish its full functional correctness. In this work, we present the first proof repair methodology for higher-order imperative functions, whose initial versions were verified in the Coq proof assistant and whose specifications remained unchanged. Our proof repair procedure is based on the combination of dynamic program alignment, enumerative invariant synthesis, and a novel technique for efficiently pruning the space of invariant candidates, dubbed proof-driven testing , enabled by the constructive nature of Coq’s proof certificates. We have implemented our approach in a mostly-automated proof repair tool called Sisyphus. Given an OCaml function verified in Coq and its unverified new version, Sisyphus produces a Coq proof for the new version, discharging most of the new proof goals automatically and suggesting high-confidence obligations for the programmer to prove for the cases when automation fails. We have evaluated Sisyphus on 10 OCaml programs taken from popular libraries, that manipulate arrays and mutable data structures, considering their verified original and unverified evolved versions. Sisyphus has managed to repair proofs for all those functions, suggesting correct invariants and generating a small number of easy-to-prove residual obligations.

APA, Harvard, Vancouver, ISO, and other styles

30

Yan, Sheng, and Wensheng Yu. "Formal Verification of a Topological Spatial Relations Model for Geographic Information Systems in Coq." Mathematics 11, no. 5 (February 21, 2023): 1079. http://dx.doi.org/10.3390/math11051079.

Full text

Abstract:

Geographic information systems have undergone rapid growth for decades. Topology has provided valuable modeling tools in the development of this field. Formal verification of the model of topological spatial relations can provide a reliable guarantee for the correctness of geographic information systems. We present a proof of the topological spatial relations model that has been formally verified in the Coq proof assistant. After an introduction to the formalization of the axiomatic set theory of Morse--Kelley, the formal description of the elementary concepts and properties of general topology is developed. The topological spatial relations between two sets are described by using the concept of the intersection value. Finally, we formally proved the topological spatial relations between two sets which are restricted to the regularly closed and the planar spatial regions. All the proof details are strictly completed in Coq, which shows that the correctness of the theoretical model for geographic information systems can be checked by a computer. This~paper provides a novel method to verify the correctness of the topological spatial relations model. This~work can also contribute to the creation and validation of various geological models and software.

APA, Harvard, Vancouver, ISO, and other styles

31

Zhou, Li, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, and Mingsheng Ying. "CoqQ: Foundational Verification of Quantum Programs." Proceedings of the ACM on Programming Languages 7, POPL (January 9, 2023): 833–65. http://dx.doi.org/10.1145/3571222.

Full text

Abstract:

CoqQ is a framework for reasoning about quantum programs in the Coq proof assistant. Its main components are: a deeply embedded quantum programming language, in which classic quantum algorithms are easily expressed, and an expressive program logic for proving properties of programs. CoqQ is foundational: the program logic is formally proved sound with respect to a denotational semantics based on state-of-art mathematical libraries (MathComp and MathComp Analysis). CoqQ is also practical: assertions can use Dirac expressions, which eases concise specifications, and proofs can exploit local and parallel reasoning, which minimizes verification effort. We illustrate the applicability of CoqQ with many examples from the literature.

APA, Harvard, Vancouver, ISO, and other styles

32

Bourke, Timothy, Basile Pesin, and Marc Pouzet. "Verified Compilation of Synchronous Dataflow with State Machines." ACM Transactions on Embedded Computing Systems 22, no. 5s (September 9, 2023): 1–26. http://dx.doi.org/10.1145/3608102.

Full text

Abstract:

Safety-critical embedded software is routinely programmed in block-diagram languages. Recent work in the Vélus project specifies such a language and its compiler in the Coq proof assistant. It builds on the CompCert verified C compiler to give an end-to-end proof linking the dataflow semantics of source programs to traces of the generated assembly code. We extend this work with switched blocks, shared variables, reset blocks, and state machines; define a relational semantics to integrate these block- and mode-based constructions into the existing stream-based model; adapt the standard source-to-source rewriting scheme to compile the new constructions; and reestablish the correctness theorem.

APA, Harvard, Vancouver, ISO, and other styles

33

Chlipala, Adam. "Skipping the binder bureaucracy with mixed embeddings in a semantics course (functional pearl)." Proceedings of the ACM on Programming Languages 5, ICFP (August 22, 2021): 1–28. http://dx.doi.org/10.1145/3473599.

Full text

Abstract:

Rigorous reasoning about programs calls for some amount of bureaucracy in managing details like variable binding, but, in guiding students through big ideas in semantics, we might hope to minimize the overhead. We describe our experiment introducing a range of such ideas, using the Coq proof assistant, without any explicit representation of variables, instead using a higher-order syntax encoding that we dub "mixed embedding": it is neither the fully explicit syntax of deep embeddings nor the syntax-free programming of shallow embeddings. Marquee examples include different takes on concurrency reasoning, including in the traditions of model checking (partial-order reduction), program logics (concurrent separation logic), and type checking (session types) -- all presented without any side conditions on variables.

APA, Harvard, Vancouver, ISO, and other styles

34

BLANQUI, FRÉDÉRIC, and ADAM KOPROWSKI. "CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates." Mathematical Structures in Computer Science 21, no. 4 (July 1, 2011): 827–59. http://dx.doi.org/10.1017/s0960129511000120.

Full text

Abstract:

Termination is an important property of programs, and is notably required for programs formulated in proof assistants. It is a very active subject of research in the Turing-complete formalism of term rewriting. Over the years, many methods and tools have been developed to address the problem of deciding termination for specific problems (since it is undecidable in general). Ensuring the reliability of those tools is therefore an important issue.In this paper we present a library formalising important results of the theory of well-founded (rewrite) relations in the proof assistant Coq. We also present its application to the automated verification of termination certificates, as produced by termination tools.The sources are freely available athttp://color.inria.fr/.

APA, Harvard, Vancouver, ISO, and other styles

35

Tassarotti, Joseph, and Jean-Baptiste Tristan. "Verified Density Compilation for a Probabilistic Programming Language." Proceedings of the ACM on Programming Languages 7, PLDI (June 6, 2023): 615–37. http://dx.doi.org/10.1145/3591245.

Full text

Abstract:

This paper presents ProbCompCert, a compiler for a subset of the Stan probabilistic programming language (PPL), in which several key compiler passes have been formally verified using the Coq proof assistant. Because of the probabilistic nature of PPLs, bugs in their compilers can be difficult to detect and fix, making verification an interesting possibility. However, proving correctness of PPL compilation requires new techniques because certain transformations performed by compilers for PPLs are quite different from other kinds of languages. This paper describes techniques for verifying such transformations and their application in ProbCompCert. In the course of verifying ProbCompCert, we found an error in the Stan language reference manual related to the semantics and implementation of a key language construct.

APA, Harvard, Vancouver, ISO, and other styles

36

Poiret, Josselin, Gaëtan Gilbert, Kenji Maillard, Pierre-Marie Pédrot, Matthieu Sozeau, Nicolas Tabareau, and Éric Tanter. "All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants." Proceedings of the ACM on Programming Languages 9, POPL (January 7, 2025): 2253–81. https://doi.org/10.1145/3704912.

Full text

Abstract:

Proof assistants based on dependent type theory, such as Coq, Lean and Agda, use different universes to classify types, typically combining a predicative hierarchy of universes for computationally-relevant types, and an impredicative universe of proof-irrelevant propositions. In general, a universe is characterized by its sort, such as Type or Prop, and its level, in the case of a predicative sort. Recent research has also highlighted the potential of introducing more sorts in the type theory of the proof assistant as a structuring means to address the coexistence of different logical or computational principles, such as univalence, exceptions, or definitional proof irrelevance. This diversity raises concrete and subtle issues from both theoretical and practical perspectives. In particular, in order to avoid duplicating definitions to inhabit all (combinations of) universes, some sort of polymorphism is needed. Universe level polymorphism is well-known and effective to deal with hierarchies, but the handling of polymorphism between sorts is currently ad hoc and limited in all major proof assistants, hampering reuse and extensibility. This work develops sort polymorphism and its metatheory, studying in particular monomorphization, large elimination, and parametricity. We implement sort polymorphism in Coq and present examples from a new sort-polymorphic prelude of basic definitions and automation. Sort polymorphism is a natural solution that effectively addresses the limitations of current approaches and prepares the ground for future multi-sorted type theories.

APA, Harvard, Vancouver, ISO, and other styles

37

Magaud, Nicolas. "Integrating an Automated Prover for Projective Geometry as a New Tactic in the Coq Proof Assistant." Electronic Proceedings in Theoretical Computer Science 336 (July 7, 2021): 40–47. http://dx.doi.org/10.4204/eptcs.336.4.

Full text

APA, Harvard, Vancouver, ISO, and other styles

38

Moiseenko, E. V., V. P. Gladstein, A. V. Podkopaev, and D. V. Koznov. "Mechanization of pomset languages in the Coq proof assistant for the specification of weak memory models." Scientific and Technical Journal of Information Technologies, Mechanics and Optics 22, no. 3 (June 1, 2022): 517–27. http://dx.doi.org/10.17586/2226-1494-2022-22-3-517-527.

Full text

APA, Harvard, Vancouver, ISO, and other styles

39

Birkedal, Lars, Thomas Dinsdale-Young, Armaël Guéneau, Guilhem Jaber, Kasper Svendsen, and Nikos Tzevelekos. "Theorems for free from separation logic specifications." Proceedings of the ACM on Programming Languages 5, ICFP (August 22, 2021): 1–29. http://dx.doi.org/10.1145/3473586.

Full text

Abstract:

Separation logic specifications with abstract predicates intuitively enforce a discipline that constrains when and how calls may be made between a client and a library. Thus a separation logic specification of a library intuitively enforces a protocol on the trace of interactions between a client and the library. We show how to formalize this intuition and demonstrate how to derive "free theorems" about such interaction traces from abstract separation logic specifications. We present several examples of free theorems. In particular, we prove that a so-called logically atomic concurrent separation logic specification of a concurrent module operation implies that the operation is linearizable. All the results presented in this paper have been mechanized and formally proved in the Coq proof assistant using the Iris higher-order concurrent separation logic framework.

APA, Harvard, Vancouver, ISO, and other styles

40

Iqbal, Saima, Wilayat Khan, Abdulrahman Alothaim, Aamir Qamar, Adi Alhudhaif, and Shtwai Alsubai. "Proving Reliability of Image Processing Techniques in Digital Forensics Applications." Security and Communication Networks 2022 (March 31, 2022): 1–17. http://dx.doi.org/10.1155/2022/1322264.

Full text

Abstract:

Binary images have found its place in many applications, such as digital forensics involving legal documents, authentication of images, digital books, contracts, and text recognition. Modern digital forensics applications involve binary image processing as part of data hiding techniques for ownership protection, copyright control, and authentication of digital media. Whether in image forensics, health, or other fields, such transformations are often implemented in high-level languages without formal foundations. The lack of formal foundation questions the reliability of the image processing techniques and hence the forensic results loose their legal significance. Furthermore, counter-forensics can impede or mislead the forensic analysis of the digital images. To ensure that any image transformation meet high standards of safety and reliability, more rigorous methods should be applied to image processing applications. To verify the reliability of these transformations, we propose to use formal methods based on theorem proving that can fulfil high standards of safety. To formally investigate binary image processing, in this paper, a reversible formal model of the binary images is defined in the Proof Assistant Coq. Multiple image transformation methods are formalized and their reliability properties are proved. To analyse real-life RGB images, a prototype translator is developed that reads RGB images and translate them to Coq definitions. As the formal definitions and proof scripts can be validated automatically by the computer, this raises the reliability and legal significance of the image forensic applications.

APA, Harvard, Vancouver, ISO, and other styles

41

BARTHE, GILLES, DAVID PICHARDIE, and TAMARA REZK. "A certified lightweight non-interference Java bytecode verifier." Mathematical Structures in Computer Science 23, no. 5 (May 17, 2013): 1032–81. http://dx.doi.org/10.1017/s0960129512000850.

Full text

Abstract:

Non-interference guarantees the absence of illicit information flow throughout program execution. It can be enforced by appropriate information flow type systems. Much of the previous work on type systems for non-interference has focused on calculi or high-level programming languages, and existing type systems for low-level languages typically omit objects, exceptions and method calls. We define an information flow type system for a sequential JVM-like language that includes all these programming features, and we prove, in the Coq proof assistant, that it guarantees non-interference. An additional benefit of the formalisation is that we have extracted from our proof a certified lightweight bytecode verifier for information flow. Our work provides, to the best of our knowledge, the first sound and certified information flow type system for such an expressive fragment of the JVM.

APA, Harvard, Vancouver, ISO, and other styles

42

RAHLI, VINCENT, and MARK BICKFORD. "Validating Brouwer's continuity principle for numbers using named exceptions." Mathematical Structures in Computer Science 28, no. 6 (November 2, 2017): 942–90. http://dx.doi.org/10.1017/s0960129517000172.

Full text

Abstract:

This paper extends the Nuprl proof assistant (a system representative of the class of extensional type theories with dependent types) withnamed exceptionsandhandlers, as well as a nominalfreshoperator. Using these new features, we prove a version of Brouwer's continuity principle for numbers. We also provide a simpler proof of a weaker version of this principle that only uses diverging terms. We prove these two principles in Nuprl's metatheory using our formalization of Nuprl in Coq and reflect these metatheoretical results in the Nuprl theory as derivation rules. We also show that these additions preserve Nuprl's key metatheoretical properties, in particular consistency and the congruence of Howe's computational equivalence relation. Using continuity and the fan theorem, we prove important results of Intuitionistic Mathematics: Brouwer's continuity theorem, bar induction on monotone bars and the negation of the law of excluded middle.

APA, Harvard, Vancouver, ISO, and other styles

43

Melquiond, Guillaume, and Josué Moreau. "A Safe Low-Level Language for Computer Algebra and Its Formally Verified Compiler." Proceedings of the ACM on Programming Languages 8, ICFP (August 15, 2024): 121–46. http://dx.doi.org/10.1145/3674629.

Full text

Abstract:

This article describes a programming language for writing low-level libraries for computer algebra systems. Such libraries (GMP, BLAS/LAPACK, etc) are usually written in C, Fortran, and Assembly, and make heavy use of arrays and pointers. The proposed language, halfway between C and Rust, is designed to be safe and to ease the deductive verification of programs, while being low-level enough to be suitable for this kind of computationally intensive applications. This article also describes a compiler for this language, based on CompCert. The safety of the language has been formally proved using the Coq proof assistant, and so has the property of semantics preservation for the compiler. While the language is not yet feature-complete, this article shows what it entails to design a new domain-specific programming language along its formally verified compiler.

APA, Harvard, Vancouver, ISO, and other styles

44

Jia, Xiaodong, Ashish Kumar, and Gang Tan. "A derivative-based parser generator for visibly Pushdown grammars." Proceedings of the ACM on Programming Languages 5, OOPSLA (October 20, 2021): 1–24. http://dx.doi.org/10.1145/3485528.

Full text

Abstract:

In this paper, we present a derivative-based, functional recognizer and parser generator for visibly pushdown grammars. The generated parser accepts ambiguous grammars and produces a parse forest containing all valid parse trees for an input string in linear time. Each parse tree in the forest can then be extracted also in linear time. Besides the parser generator, to allow more flexible forms of the visibly pushdown grammars, we also present a translator that converts a tagged CFG to a visibly pushdown grammar in a sound way, and the parse trees of the tagged CFG are further produced by running the semantic actions embedded in the parse trees of the translated visibly pushdown grammar. The performance of the parser is compared with a popular parsing tool ANTLR and other popular hand-crafted parsers. The correctness of the core parsing algorithm is formally verified in the proof assistant Coq.

APA, Harvard, Vancouver, ISO, and other styles

45

Bagnall, Alexander, Gordon Stewart, and Anindya Banerjee. "Formally Verified Samplers from Probabilistic Programs with Loops and Conditioning." Proceedings of the ACM on Programming Languages 7, PLDI (June 6, 2023): 1–24. http://dx.doi.org/10.1145/3591220.

Full text

Abstract:

We present Zar: a formally verified compiler pipeline from discrete probabilistic programs with unbounded loops in the conditional probabilistic guarded command language (cpGCL) to proved-correct executable samplers in the random bit model. We exploit the key idea that all discrete probability distributions can be reduced to unbiased coin-flipping schemes. The compiler pipeline first translates cpGCL programs into choice-fix trees, an intermediate representation suitable for reduction of biased probabilistic choices. Choice-fix trees are then translated to coinductive interaction trees for execution within the random bit model. The correctness of the composed translations establishes the sampling equidistribution theorem: compiled samplers are correct wrt. the conditional weakest pre-expectation semantics of cpGCL source programs. Zar is implemented and fully verified in the Coq proof assistant. We extract verified samplers to OCaml and Python and empirically validate them on a number of illustrative examples.

APA, Harvard, Vancouver, ISO, and other styles

46

Liu, Yiyun, Jonathan Chan, and Stephanie Weirich. "Consistency of a Dependent Calculus of Indistinguishability." Proceedings of the ACM on Programming Languages 9, POPL (January 7, 2025): 183–209. https://doi.org/10.1145/3704843.

Full text

Abstract:

The Dependent Calculus of Indistinguishability (DCOI) uses dependency tracking to identify irrelevant arguments and uses indistinguishability during type conversion to enable proof irrelevance, supporting run-time and compile-time irrelevance with the same uniform mechanism. DCOI also internalizes reasoning about indistinguishability through the use of a propositional equality type indexed by an observer level. As DCOI is a pure type system, prior work establishes only its syntactic type safety, justifying its use as the basis for a programming language with dependent types. However, it was not clear whether any instance of this system would be suitable for use as a type theory for theorem proving. Here, we identify a suitable instance DCOI ω , which has an infinite predicative universe hierarchy. We show that DCOI ω is logically consistent, normalizing, and that type conversion is decidable. We have mechanized all results using the Coq proof assistant.

APA, Harvard, Vancouver, ISO, and other styles

47

Muller, Jean-Michel, and Laurence Rideau. "Formalization of Double-Word Arithmetic, and Comments on “Tight and Rigorous Error Bounds for Basic Building Blocks of Double-Word Arithmetic”." ACM Transactions on Mathematical Software 48, no. 1 (March 31, 2022): 1–24. http://dx.doi.org/10.1145/3484514.

Full text

Abstract:

Recently, a complete set of algorithms for manipulating double-word numbers (some classical, some new) was analyzed [ 16 ]. We have formally proven all the theorems given in that article, using the Coq proof assistant. The formal proof work led us to: (i) locate mistakes in some of the original paper proofs (mistakes that, however, do not hinder the validity of the algorithms), (ii) significantly improve some error bounds, and (iii) generalize some results by showing that they are still valid if we slightly change the rounding mode. The consequence is that the algorithms presented in [ 16 ] can be used with high confidence, and that some of them are even more accurate than what was believed before. This illustrates what formal proof can bring to computer arithmetic: beyond mere (yet extremely useful) verification, correction, and consolidation of already known results, it can help to find new properties. All our formal proofs are freely available.

APA, Harvard, Vancouver, ISO, and other styles

48

FILLIÂTRE, JEAN-CHRISTOPHE. "Verification of non-functional programs using interpretations in type theory." Journal of Functional Programming 13, no. 4 (June 25, 2003): 709–45. http://dx.doi.org/10.1017/s095679680200446x.

Full text

Abstract:

We study the problem of certifying programs combining imperative and functional features within the general framework of type theory. Type theory is a powerful specification language which is naturally suited for the proof of purely functional programs. To deal with imperative programs, we propose a logical interpretation of an annotated program as a partial proof of its specification. The construction of the corresponding partial proof term is based on a static analysis of the effects of the program which excludes aliases. The missing subterms in the partial proof term are seen as proof obligations, whose actual proofs are left to the user. We show that the validity of those proof obligations implies the total correctness of the program. This work has been implemented in the Coq proof assistant. It appears as a tactic taking an annotated program as argument and generating a set of proof obligations. Several nontrivial algorithms have been certified using this tactic.

APA, Harvard, Vancouver, ISO, and other styles

49

Dejon, Nicolas, Chrystel Gaber, and Gilles Grimaud. "Pip-MPU: Formal Verification of an MPU-Based Separationkernel for Constrained Devices." International Journal of Embedded Systems and Applications 13, no. 02 (June 27, 2023): 1–21. http://dx.doi.org/10.5121/ijesa.2023.13201.

Full text

Abstract:

Pip-MPU is a minimalist separation kernel for constrained devices (scarce memory and power resources).In this work, we demonstrate high-assurance of Pip-MPU’s isolation property through formal verification.Pip-MPU offers user-defined on-demand multiple isolation levels guarded by the Memory Protection Unit (MPU).Pip-MPU derives from the Pip protokernel, with a full code refactoring to adapt to the constrained environment and targets equivalent security properties.The proofs verify that the memory blocks loaded in the MPU adhere to the global partition tree model.We provide the basis of the MPU formalisation and the demonstration of the formal verification strategy on two representative kernel services.The publicly released proofs have been implemented and checked using the Coq Proof Assistant for three kernel services, representing around 10000 lines of proof.To our knowledge, this is the first formal verification of an MPU-based separation kernel.The verification process helped discover a critical isolation-related bug.

APA, Harvard, Vancouver, ISO, and other styles

50

Gregersen, Simon Oddershede, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, and Lars Birkedal. "Asynchronous Probabilistic Couplings in Higher-Order Separation Logic." Proceedings of the ACM on Programming Languages 8, POPL (January 5, 2024): 753–84. http://dx.doi.org/10.1145/3632868.

Full text

Abstract:

Probabilistic couplings are the foundation for many probabilistic relational program logics and arise when relating random sampling statements across two programs. In relational program logics, this manifests as dedicated coupling rules that, e.g., say we may reason as if two sampling statements return the same value. However, this approach fundamentally requires aligning or "synchronizing" the sampling statements of the two programs which is not always possible. In this paper, we develop Clutch, a higher-order probabilistic relational separation logic that addresses this issue by supporting asynchronous probabilistic couplings. We use Clutch to develop a logical step-indexed logical relation to reason about contextual refinement and equivalence of higher-order programs written in a rich language with a probabilistic choice operator, higher-order local state, and impredicative polymorphism. Finally, we demonstrate our approach on a number of case studies. All the results that appear in the paper have been formalized in the Coq proof assistant using the Coquelicot library and the Iris separation logic framework.

APA, Harvard, Vancouver, ISO, and other styles

Journal articles on the topic 'Coq (assistant de preuve)'

Create a spot-on reference in APA, MLA, Chicago, Harvard, and other styles