Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
From MaRDI portal
Publication:703860
zbMath1069.68095MaRDI QIDQ703860
Publication date: 12 January 2005
Published in: Texts in Theoretical Computer Science. An EATCS Series (Search for Journal in Brave)
Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35)
Related Items
An Assertional Proof of the Stability and Correctness of Natural Mergesort, A Formalization of Properties of Continuous Functions on Closed Intervals, Semantic Foundations for Deterministic Dataflow and Stream Processing, Deep Generation of Coq Lemma Names Using Elaborated Terms, Fold–unfold lemmas for reasoning about recursive programs using the Coq proof assistant, Computational logic: its origins and applications, Getting There and Back Again, Algebraic data integration, Characteristics of de Bruijn’s early proof checker Automath, Unnamed Item, Fundamentals of compositional rewriting theory, Folding left and right matters: Direct style, accumulators, and continuations, An automatically verified prototype of the Android permissions system, Verifiable decryption in the head, Formalizing Some “Small” Finite Models of Projective Geometry in Coq, Machine Learning for Inductive Theorem Proving, Towards a practical library for monadic equational reasoning in Coq, Embedded domain specific verifiers, Formal verification of termination criteria for first-order recursive functions, Efficient computation of arbitrary control dependencies, Region-based resource management and lexical exception handlers in continuation-passing style, \textsf{LOGIC}: a Coq library for logics, Completeness and the finite model property for Kleene algebra, reconsidered, \textsf{symQV}: automated symbolic verification of quantum programs, Squeezing streams and composition of self-stabilizing algorithms, Unnamed Item, Mtac: A monad for typed tactic programming in Coq, Unnamed Item, Unnamed Item, Unnamed Item, Idris, a general-purpose dependently typed programming language: Design and implementation, Validating Brouwer's continuity principle for numbers using named exceptions, An insider's look at LF type reconstruction: everything you (n)ever wanted to know, The Strategy Challenge in SMT Solving, Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting, Mechanized Verification of Computing Dominators for Formalizing Compilers, Common Knowledge Logic in a Higher Order Proof Assistant, Simulating Finite Eilenberg Machines with a Reactive Engine, Implementing Real Numbers With RZ, Automatically inferring loop invariants via algorithmic learning, A univalent formalization of the p-adic numbers, Partiality and recursion in interactive theorem provers – an overview, An extensible approach to session polymorphism, Verified Compilation and the B Method: A Proposal and a First Appraisal, A case-study in algebraic manipulation using mechanized reasoning tools, Introduction to Type Theory, Dependent Types at Work, Structural Abstract Interpretation: A Formal Study Using Coq, Fast and correctly rounded logarithms in double-precision, Calculational relation-algebraic proofs in the teaching tool \textsc{CalcCheck}, Incidence Simplicial Matrices Formalized in Coq/SSReflect, Computer Certified Efficient Exact Reals in Coq, A Foundational View on Integration Problems, Verifying safety critical task scheduling systems in PPTL axiom system, Mechanical Theorem Proving in Tarski’s Geometry, The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem, Unnamed Item, Synchronous gathering without multiplicity detection: a certified algorithm, Folding left and right over Peano numbers, Combining Coq and Gappa for Certifying Floating-Point Programs, Formal Proof: Reconciling Correctness and Understanding, Finite Groups Representation Theory with Coq, First-Class Object Sets, Using Structural Recursion for Corecursion, A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq, Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus, An induction principle for nested datatypes in intensional type theory, Building Mathematics-Based Software Systems to Advance Science and Create Knowledge, Axiomatic and dual systems for constructive necessity, a formally verified equivalence, Libraries for Generic Programming in Haskell, A Formal, Resource Consumption-Preserving Translation from Actors with Cooperative Scheduling to Haskell*, On Correctness of Mathematical Texts from a Logical and Practical Point of View, Program Testing and the Meaning Explanations of Intuitionistic Type Theory, Coalgebras as Types Determined by Their Elimination Rules, Proof Auditing Formalised Mathematics, A focused linear logical framework and its application to metatheory of object logics, Certifying choreography compilation, Category theory, logic and formal linguistics: some connections, old and new, A model of type theory in simplicial sets. A brief introduction to Voevodsky's homotopy type theory, How testing helps to diagnose proof failures, Tests and proofs for custom data generators, The reflective Milawa theorem prover is sound (down to the machine code that runs it), The effects of effects on constructivism, Towards a certified version of the encyclopedia of triangle centers, An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps, Coq formalization of the higher-order recursive path ordering, Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques, A minimalistic look at widening operators, Ordinal arithmetic: Algorithms and mechanization, Generalized arrays for Stainless frames, Trace semantics and algebraic laws for MCA ARMv8 architecture based on UTP, Floating-point arithmetic on the test bench. How are verified numerical solutions calculated?, Program logic for higher-order probabilistic programs in Isabelle/HOL, Innovations in computational type theory using Nuprl, \textit{Theorema}: Towards computer-aided mathematical theory exploration, A two-valued logic for properties of strict functional programs allowing partial functions, Wave equation numerical resolution: a comprehensive mechanized proof of a C program, Hammer for Coq: automation for dependent type theory, The ILTP problem library for intuitionistic logic, A complete proof system for propositional projection temporal logic, A scalable module system, Intuitionistic completeness of first-order logic, Formal specification and proofs for the topology and classification of combinatorial surfaces, Deadlock and starvation free reentrant readers-writers: a case study combining model checking with theorem proving, Trace-based verification of imperative programs with I/O, How to get more out of your oracles, Typing total recursive functions in Coq, Schulze voting as evidence carrying computation, Foundational aspects of multiscale digitization, A complete axiom system for propositional projection temporal logic with cylinder computation model, Formally proving size optimality of sorting networks, Sorting nine inputs requires twenty-five comparisons, Map fusion for nested datatypes in intensional type theory, Effective homology of bicomplexes, formalized in Coq, A list-machine benchmark for mechanized metatheory, A semantic framework for proof evidence, \(\lim +, \delta^+\), and non-permutability of \(\beta\)-steps, Experiments in program verification using Event-B, The matrix reproved (verification pearl), Formal verification of numerical programs: from C annotated programs to mechanical proofs, Adding logic to the toolbox of molecular biology, The area method. A recapitulation, Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax, Coalgebras in functional programming and type theory, A case study in formalizing projective geometry in Coq: Desargues theorem, Designing and proving correct a convex hull algorithm with hypermaps in Coq, Verification conditions for source-level imperative programs, From types to sets by local type definition in higher-order logic, Representing model theory in a type-theoretical logical framework, A mechanized proof of the basic perturbation lemma, Tilting at windmills with Coq: Formal verification of a compilation algorithm for parallel moves, A mechanical analysis of program verification strategies, Recycling proof patterns in Coq: case studies, Formalizing non-interference for a simple bytecode language in Coq, Impossibility of gathering, a certification, Formal study of functional orbits in finite domains, Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits, A consistent foundation for Isabelle/HOL, Polyhedra genus theorem and Euler formula: A hypermap-formalized intuitionistic proof, Formal verification of a C-like memory model and its uses for verifying program transformations, Proof synthesis and reflection for linear arithmetic, An assertional proof of red-black trees using Dafny, A language-independent proof system for full program equivalence, A formal semantics of nested atomic sections with thread escape, Cut branches before looking for bugs: certifiably sound verification on relaxed slices, Automated deduction and knowledge management in geometry, (Co)inductive proof systems for compositional proofs in reachability logic, Optimization techniques for propositional intuitionistic logic and their implementation, A framework for developing stand-alone certifiers, A verified framework for higher-order uncurrying optimizations, Partial and nested recursive function definitions in higher-order logic, Formal proofs of rounding error bounds. With application to an automatic positive definiteness check, Coquelicot: a user-friendly library of real analysis for Coq, Floating-point arithmetic in the Coq system, ``Backward coinduction, Nash equilibrium and the rationality of escalation, A formally verified floating-point implementation of the compact position reporting algorithm, A computer-verified monadic functional implementation of the integral, A generic and executable formalization of signature-based Gröbner basis algorithms, TacticToe: learning to prove with tactics, Undecidability of equality for codata types, Implementing type systems for the IDE with Xsemantics, Certified abstract cost analysis, Implementing geometric algebra products with binary trees, A formal proof of the deadline driven scheduler in PPTL axiomatic system, Coinductive big-step operational semantics, Certifying properties of an efficient functional program for computing Gröbner bases, Distilling the requirements of Gödel's incompleteness theorems with a proof assistant, A symbolic-numeric validation algorithm for linear ODEs with Newton-Picard method, Using computer algebra techniques for the specification, verification and synthesis of recursive programs, Adapting functional programs to higher order logic, A compact kernel for the calculus of inductive constructions, Integrating induction and coinduction via closure operators and proof cycles, Verifying Whiley programs with Boogie, Flexible proof production in an industrial-strength SMT solver, \textsc{Prawf}: an interactive proof system for program extraction, \texttt{slepice}: towards a verified implementation of type theory in type theory, Theorem proving graph grammars with attributes and negative application conditions, Using relation-algebraic means and tool support for investigating and computing bipartitions, Analyzing program termination and complexity automatically with \textsf{AProVE}, Let’s See How Things Unfold: Reconciling the Infinite with the Intensional (Extended Abstract), Semantic representation of general topology in the Wolfram language, Automatically proving equivalence by type-safe reflection, Towards Logical Frameworks in the Heterogeneous Tool Set Hets, Automating Induction with an SMT Solver, Two cryptomorphic formalizations of projective incidence geometry, Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof, Introduction to Model Checking, Combining Model Checking and Deduction, SEPIA: Search for Proofs Using Inferred Automata, Inductive Beluga: Programming Proofs, Bisimulations Generated from Corecursive Equations, Extracting a DPLL Algorithm, Invariants for the FoCaL language, A Brief Overview of Agda – A Functional Language with Dependent Types, Acyclic Preferences and Existence of Sequential Nash Equilibria: A Formal and Constructive Equivalence, Trace-Based Coinductive Operational Semantics for While, Formal Verification of Exact Computations Using Newton’s Method, Deciding Regular Expressions (In-)Equivalence in Coq, Rationality Authority for Provable Rational Behavior, A decision procedure for linear ``big O equations, Code-carrying theories, Mechanizing common knowledge logic using COQ, Design and formal proof of a new optimal image segmentation program with hypermaps, A brief account of runtime verification, A two-level logic approach to reasoning about computations, Translation certification for smart contracts, Trusting computations: a mechanized proof from partial differential equations to actual program, Mechanized semantics for the clight subset of the C language, A formally verified compiler back-end, Crystal: Integrating structured queries into a tactic language, Deletion: The curse of the red-black tree, Homotopy type theory and Voevodsky’s univalent foundations, Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge, Extensional higher-order paramodulation in Leo-III, A Consistent Foundation for Isabelle/HOL, Intuitionistic Ancestral Logic as a Dependently Typed Abstract Programming Language, Mechanized Verification of CPS Transformations, CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types, In the Search of a Naive Type Theory, Certification of an exact worst-case self-stabilization time, Verifying a scheduling protocol of safety-critical systems, Theoretical and practical approaches to the denotational semantics for MDESL based on UTP, Verification of the ROS NavFn planner using executable specification languages, Some issues related to double rounding, UTPCalc — A Calculator for UTP Predicates, Formalization of real analysis: a survey of proof assistants and libraries, Relational characterisations of paths, Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support, SMT proof checking using a logical framework, Friends with Benefits, Comprehending Isabelle/HOL’s Consistency, On Choice Rules in Dependent Type Theory, A Short Presentation of Coq, Canonical Big Operators, MikiBeta : A General GUI Library for Visualizing Proof Trees, Para-Disagreement Logics and Their Implementation Through Embedding in Coq and SMT, From Mathesis Universalis to Provability, Computability, and Constructivity, Fixpoints and Search in PVS, Balancing weight-balanced trees, A characterization of Moessner's sieve, The dodecahedral conjecture, A Machine Checked Soundness Proof for an Intermediate Verification Language, Formal Modelling of Emotions in BDI Agents, From LCF to Isabelle/HOL, A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs, Reasoning in Abella about Structural Operational Semantics Specifications, Another Look at Function Domains, Partial Derivative Automata Formalized in Coq, Theorem-proving analysis of digital control logic interacting with continuous dynamics, On the Formalization of Some Results of Context-Free Language Theory, A Polymorphic Type System for the Lambda-Calculus with Constructors, Formal proofs for theoretical properties of Newton's method, A formal study of Bernstein coefficients and polynomials, Type classes for mathematics in type theory, A pluralist approach to the formalisation of mathematics, Tests and Proofs for Enumerative Combinatorics, Mechanical Verification of a Constructive Proof for FLP, From Types to Sets by Local Type Definitions in Higher-Order Logic, Hardware-Dependent Proofs of Numerical Programs, A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry, Mechanized metatheory revisited, Formally verifying the solution to the Boolean Pythagorean triples problem, Formalization of geometric algebra in HOL Light, Statistical properties of lambda terms, Mechanizing focused linear logic in Coq, Interactive verification of architectural design patterns in FACTum, Semantic Determinism and Functional Logic Program Properties, Tool Support for Proof Engineering, Deciding Kleene algebra terms equivalence in Coq, Automated formal analysis and verification: an overview, A framework for the verification of certifying computations, Theorem of three circles in Coq, Inductive and Coinductive Components of Corecursive Functions in Coq, Premise selection for mathematics by corpus analysis and kernel methods, Formally verified certificate checkers for hardest-to-round computation, Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective
Uses Software
