A Declarative Language for the Coq Proof Assistant
From MaRDI portal
Publication:3499750
DOI10.1007/978-3-540-68103-8_5zbMath1138.68525OpenAlexW2134919871MaRDI QIDQ3499750
Publication date: 3 June 2008
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-68103-8_5
Related Items
A complete semantics of \(\mathbb{K}\) and its translation to Isabelle ⋮ Four decades of {\textsc{Mizar}}. Foreword ⋮ Improving legibility of formal proofs based on the close reference principle is NP-hard ⋮ Proof-checking Euclid ⋮ Mizar: State-of-the-art and Beyond ⋮ A Brief Overview of Mizar ⋮ Declarative representation of proof terms ⋮ Crystal: Integrating structured queries into a tactic language ⋮ Automating formalization by statistical and semantic parsing of mathematics ⋮ Weak call-by-value lambda calculus as a model of computation in Coq ⋮ Categoricity results for second-order ZF in dependent type theory ⋮ Formalization of functional variation in HOL Light ⋮ A certified proof of the Cartan fixed point theorems ⋮ Disjoint Polymorphism ⋮ Declarative Proof Translation (Short Paper) ⋮ A denotational semantics of textually aligned SPMD programs ⋮ Large Formal Wikis: Issues and Solutions ⋮ Towards Formal Proof Script Refactoring ⋮ Program Calculation in Coq ⋮ Unnamed Item ⋮ A Logically Saturated Extension of ${{\bar\lambda\mu\tilde{\mu}}}$ ⋮ Call-by-value lambda calculus as a model of computation in Coq ⋮ Semantics of Mizar as an Isabelle object logic ⋮ Formalizing in Coq Hidden Algebras to Specify Symbolic Computation Systems
Uses Software
Cites Work
