A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL

DOI10.1007/S10817-011-9231-4zbMATH Open1260.68366OpenAlexW2077540255MaRDI QIDQ1945915FDOQ1945915

Stefan Berghofer

Publication date: 17 April 2013

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-011-9231-4

zbMATH Keywords

lambda calculustype systemsformalized metatheory

Mathematics Subject Classification ID

Theory of programming languages (68N15) Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18)

Cites Work

• Theorem Proving in Higher Order Logics
• Isabelle/HOL. A proof assistant for higher-order logic
• More Church-Rosser proofs (in Isabelle/HOL)
• Types and programing languages
• Automated Deduction – CADE-20
• Types for Proofs and Programs
• Residual theory in λ-calculus: a formal development
• Turning Inductive into Equational Specifications
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (1)

• A solution to the PoplMark challenge based on de Bruijn indices

Uses Software

• Coq
• ML
• Isabelle/HOL
• Twelf
• PoplMark
• Nominal Isabelle

This page was built for publication: A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1945915)