From types to sets by local type definition in higher-order logic
type: Item
instance of: scholarly article
title: From types to sets by local type definition in higher-order logic
zbMATH Open document ID: 1468.68295
author: Ondřej Kunčar
author: Andrei Popescu
published in: Journal of Automated Reasoning
publication date: 2019-02-18T00:00:00Z
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7024458
zbMATH Keywords: HOL
zbMATH Keywords: Isabelle
zbMATH Keywords: local typedef
zbMATH Keywords: type definition
zbMATH Keywords: relativization
zbMATH Keywords: type classes
zbMATH Keywords: overloading
zbMATH Keywords: dependent types
zbMATH Keywords: consistency
zbMATH Keywords: transfer
zbMATH Keywords: type-based theorems
zbMATH Keywords: set-based theorems
describes a project that uses: Agda
describes a project that uses: Isabelle/HOL
describes a project that uses: Locales
describes a project that uses: Mizar
describes a project that uses: Matita
describes a project that uses: ML
describes a project that uses: HOL
describes a project that uses: HOL Light
describes a project that uses: HOL-Omega
describes a project that uses: Coq
describes a project that uses: Isabelle
describes a project that uses: Nuprl
describes a project that uses: HOL Zero
describes a project that uses: Transfer
describes a project that uses: Lifting
describes a project that uses: Berlekamp Zassenhaus
MaRDI profile type: Publication
full work available at URL: s10817-018-9464-6
OpenAlex ID: W2806477068
cites work: From Types to Sets by Local Type Definitions in Higher-Order Logic
cites work: A Brief Overview of Agda – A Functional Language with Dependent Types
cites work: Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
cites work: The Matita Interactive Theorem Prover
cites work: Isabelle/HOL. A proof assistant for higher-order logic
cites work: Mizar: State-of-the-art and Beyond
cites work: The HOL-Omega Logic
cites work: A mechanized proof of the basic perturbation lemma
cites work: Mechanisation of AKS Algorithm: Part 1 – The Main Theorem
cites work: Three Chapters of Measure Theory in Isabelle/HOL
cites work: A formalization of metric spaces in HOL Light
cites work: Q5287513
cites work: Comprehending Isabelle/HOL’s Consistency
cites work: Constructive Type Classes in Isabelle
cites work: A Mechanized Translation from Higher-Order Logic to Set Theory
cites work: Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
cites work: Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving
cites work: The HOL Light theory of Euclidean space
cites work: Theorem Proving in Higher Order Logics
cites work: A verified implementation of the Berlekamp-Zassenhaus factorization algorithm
cites work: Locales: a module system for mathematical theories
DOI: 10.1007/S10817-018-9464-6
description: scientific article; zbMATH DE number 7024458