A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL
type: Item
instance of: scholarly article
title: A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL
zbMATH Open document ID: 1260.68366
author: Stefan Berghofer
published in: Journal of Automated Reasoning
publication date: 2013-04-17T00:00:00Z
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 68N18
Mathematics Subject Classification ID: 68N15
zbMATH DE Number: 6154937
zbMATH Keywords: lambda calculus
zbMATH Keywords: type systems
zbMATH Keywords: formalized metatheory
describes a project that uses: ML
describes a project that uses: Isabelle/HOL
describes a project that uses: Coq
describes a project that uses: Twelf
describes a project that uses: PoplMark
describes a project that uses: Nominal Isabelle
MaRDI profile type: Publication
full work available at URL: s10817-011-9231-4
OpenAlex ID: W2077540255
cites work: Theorem Proving in Higher Order Logics
cites work: Q3075242
cites work: Types for Proofs and Programs
cites work: Turning Inductive into Equational Specifications
cites work: Q4736387
cites work: Residual theory in λ-calculus: a formal development
cites work: More Church-Rosser proofs (in Isabelle/HOL)
cites work: Isabelle/HOL. A proof assistant for higher-order logic
cites work: Q5687569
cites work: Types and programing languages
cites work: Automated Deduction – CADE-20
DOI: 10.1007/S10817-011-9231-4
description: scientific article; zbMATH DE number 6154937