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)
68-01: Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science
68N18: Functional programming and lambda calculus
03B70: Logic in computer science
68Q60: Specification and verification (program logics, model checking, etc.)
03B35: Mechanization of proofs and logical operations
Related Items
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, The reflective Milawa theorem prover is sound (down to the machine code that runs it), Towards a certified version of the encyclopedia of triangle centers, Floating-point arithmetic on the test bench. How are verified numerical solutions calculated?, 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, 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, \(\lim +, \delta^+\), and non-permutability of \(\beta\)-steps, Experiments in program verification using Event-B, The area method. A recapitulation, Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax, 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, Recycling proof patterns in Coq: case studies, Impossibility of gathering, a certification, Formal study of functional orbits in finite domains, A language-independent proof system for full program equivalence, A framework for developing stand-alone certifiers, 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, Map fusion for nested datatypes in intensional type theory, Effective homology of bicomplexes, formalized in Coq, Coalgebras in functional programming and type theory, Representing model theory in a type-theoretical logical framework, Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits, Cut branches before looking for bugs: certifiably sound verification on relaxed slices, Floating-point arithmetic in the Coq system, ``Backward coinduction, Nash equilibrium and the rationality of escalation, Implementing type systems for the IDE with Xsemantics, Implementing geometric algebra products with binary trees, A formal proof of the deadline driven scheduler in PPTL axiomatic system, 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, A minimalistic look at widening operators, Ordinal arithmetic: Algorithms and mechanization, Innovations in computational type theory using Nuprl, \textit{Theorema}: Towards computer-aided mathematical theory exploration, The ILTP problem library for intuitionistic logic, A complete axiom system for propositional projection temporal logic with cylinder computation model, Sorting nine inputs requires twenty-five comparisons, 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, Formalizing non-interference for a simple bytecode language in Coq, 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, Optimization techniques for propositional intuitionistic logic and their implementation, A verified framework for higher-order uncurrying optimizations, Partial and nested recursive function definitions in higher-order logic, A computer-verified monadic functional implementation of the integral, Coinductive big-step operational semantics, Certifying properties of an efficient functional program for computing Gröbner bases, 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, How testing helps to diagnose proof failures, Tests and proofs for custom data generators, Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques, Hammer for Coq: automation for dependent type theory, How to get more out of your oracles, Typing total recursive functions in Coq, Schulze voting as evidence carrying computation, Formally proving size optimality of sorting networks, A semantic framework for proof evidence, The matrix reproved (verification pearl), Adding logic to the toolbox of molecular biology, From types to sets by local type definition in higher-order logic, A consistent foundation for Isabelle/HOL, A formal semantics of nested atomic sections with thread escape, Undecidability of equality for codata types, Foundational aspects of multiscale digitization, A list-machine benchmark for mechanized metatheory, Formal verification of numerical programs: from C annotated programs to mechanical proofs, An assertional proof of red-black trees using Dafny, Automated deduction and knowledge management in geometry, (Co)inductive proof systems for compositional proofs in reachability 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, A formally verified floating-point implementation of the compact position reporting algorithm, A generic and executable formalization of signature-based Gröbner basis algorithms, TacticToe: learning to prove with tactics, Certified abstract cost analysis, 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, 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, Certifying choreography compilation, The effects of effects on constructivism, Generalized arrays for Stainless frames, Trace semantics and algebraic laws for MCA ARMv8 architecture based on UTP, Program logic for higher-order probabilistic programs in Isabelle/HOL, Translation certification for smart contracts, Theoretical and practical approaches to the denotational semantics for MDESL based on UTP, Relational characterisations of paths, Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support, A characterization of Moessner's sieve, From LCF to Isabelle/HOL, 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, Deciding Kleene algebra terms equivalence in Coq, A framework for the verification of certifying computations, Theorem of three circles 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, 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}, Semantic representation of general topology in the Wolfram language, Automatically proving equivalence by type-safe reflection, Invariants for the FoCaL language, A brief account of runtime verification, A two-level logic approach to reasoning about computations, Trusting computations: a mechanized proof from partial differential equations to actual program, Verifying a scheduling protocol of safety-critical systems, Some issues related to double rounding, SMT proof checking using a logical framework, Theorem-proving analysis of digital control logic interacting with continuous dynamics, Two cryptomorphic formalizations of projective incidence geometry, 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, Mechanized semantics for the clight subset of the C language, A formally verified compiler back-end, Crystal: Integrating structured queries into a tactic language, Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge, Extensional higher-order paramodulation in Leo-III, Certification of an exact worst-case self-stabilization time, Verification of the ROS NavFn planner using executable specification languages, 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, On the Formalization of Some Results of Context-Free Language Theory, 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, Semantic Determinism and Functional Logic Program Properties, Tool Support for Proof Engineering, Automated formal analysis and verification: an overview, Inductive and Coinductive Components of Corecursive Functions in Coq, Let’s See How Things Unfold: Reconciling the Infinite with the Intensional (Extended Abstract), Towards Logical Frameworks in the Heterogeneous Tool Set Hets, Automating Induction with an SMT Solver, Deciding Regular Expressions (In-)Equivalence in Coq, Deletion: The curse of the red-black tree, Homotopy type theory and Voevodsky’s univalent foundations, A Consistent Foundation for Isabelle/HOL, Intuitionistic Ancestral Logic as a Dependently Typed Abstract Programming Language, UTPCalc — A Calculator for UTP Predicates, Formalization of real analysis: a survey of proof assistants and libraries, Friends with Benefits, Comprehending Isabelle/HOL’s Consistency, On Choice Rules in Dependent Type Theory, MikiBeta : A General GUI Library for Visualizing Proof Trees, Balancing weight-balanced trees, Partial Derivative Automata Formalized in Coq, 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, Hardware-Dependent Proofs of Numerical Programs, A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry, Introduction to Model Checking, Combining Model Checking and Deduction, Bisimulations Generated from Corecursive Equations, Extracting a DPLL Algorithm, 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, Para-Disagreement Logics and Their Implementation Through Embedding in Coq and SMT, From Mathesis Universalis to Provability, Computability, and Constructivity, Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof, SEPIA: Search for Proofs Using Inferred Automata, Inductive Beluga: Programming Proofs, Rationality Authority for Provable Rational Behavior, 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, A Short Presentation of Coq, Canonical Big Operators, Fixpoints and Search in PVS, The dodecahedral conjecture, A Machine Checked Soundness Proof for an Intermediate Verification Language, Formal Modelling of Emotions in BDI Agents, A Polymorphic Type System for the Lambda-Calculus with Constructors, Computational logic: its origins and applications, Algebraic data integration, Validating Brouwer's continuity principle for numbers using named exceptions, Unnamed Item, Unnamed Item, Unnamed Item, An insider's look at LF type reconstruction: everything you (n)ever wanted to know, The Strategy Challenge in SMT Solving, Mechanized Verification of Computing Dominators for Formalizing Compilers, Common Knowledge Logic in a Higher Order Proof Assistant, Implementing Real Numbers With RZ, Unnamed Item, Folding left and right over Peano numbers, A Formal, Resource Consumption-Preserving Translation from Actors with Cooperative Scheduling to Haskell*, A focused linear logical framework and its application to metatheory of object logics, 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, Getting There and Back Again, Characteristics of de Bruijn’s early proof checker Automath, Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting, Simulating Finite Eilenberg Machines with a Reactive Engine, Verified Compilation and the B Method: A Proposal and a First Appraisal, Introduction to Type Theory, Dependent Types at Work, Structural Abstract Interpretation: A Formal Study Using Coq, Incidence Simplicial Matrices Formalized in Coq/SSReflect, Computer Certified Efficient Exact Reals in Coq, A Foundational View on Integration Problems, The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem, Axiomatic and dual systems for constructive necessity, a formally verified equivalence, Program Testing and the Meaning Explanations of Intuitionistic Type Theory, Coalgebras as Types Determined by Their Elimination Rules, Proof Auditing Formalised Mathematics, An Assertional Proof of the Stability and Correctness of Natural Mergesort, Mtac: A monad for typed tactic programming in Coq, Idris, a general-purpose dependently typed programming language: Design and implementation, Fast and correctly rounded logarithms in double-precision, Mechanical Theorem Proving in Tarski’s Geometry, On Correctness of Mathematical Texts from a Logical and Practical Point of View, 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, A case-study in algebraic manipulation using mechanized reasoning tools, Calculational relation-algebraic proofs in the teaching tool \textsc{CalcCheck}, Verifying safety critical task scheduling systems in PPTL axiom system, Synchronous gathering without multiplicity detection: a certified algorithm, Unnamed Item, 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, 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, Libraries for Generic Programming in Haskell
Uses Software
