Isabelle/HOL. A proof assistant for higher-order logic
type: Item
instance of: scholarly article
title: Isabelle/HOL. A proof assistant for higher-order logic
zbMATH Open document ID: 0994.68131
author: Tobias Nipkow
author: Markus Wenzel
author: Lawrence C. Paulson
published in: Lecture Notes in Computer Science
publication date: 2002-06-12T00:00:00Z
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 68-02
Mathematics Subject Classification ID: 03B35
zbMATH DE Number: 1754490
zbMATH Keywords: Isabelle
describes a project that uses: Haskell
describes a project that uses: HOL
describes a project that uses: Isabelle
describes a project that uses: Proof General
describes a project that uses: Isabelle/HOL
MaRDI profile type: Publication
Recommended article: Q4823141
Recommended article: Programming and verifying a declarative first-order prover in Isabelle/HOL
Recommended article: Q5287513
Recommended article: Higher-Order Separation Logic in Isabelle/HOLCF
Recommended article: A proof strategy language and proof script generation for Isabelle/HOL
Recommended article: Isabelle as Document-Oriented Proof Assistant
Recommended article: Isabelle/HOL/GST: a formal proof environment for generalized set theories
Recommended article: Automatic Proof and Disproof in Isabelle/HOL
Recommended article: Formalizing axiomatic systems for propositional logic in Isabelle/HOL
Recommended article: A consistent foundation for Isabelle/HOL
description: scientific article; zbMATH DE number 1754490