Mechanizing metatheory without typing contexts

DOI10.1007/s10817-013-9287-4zbMath1332.68203OpenAlexW2052151316MaRDI QIDQ2352491

Gyesik Lee, Sungwoo Park, Jeongbong Seo, Jong Hyun Park

Publication date: 2 July 2015

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

Full work available at URL: https://doi.org/10.1007/s10817-013-9287-4

zbMATH Keywords

\textsc{ {PoplMark}}System \(\mathrm{F}_{<:}\)typing context

Mathematics Subject Classification ID

Related Items (2)

Extensional proofs in a propositional logic modulo isomorphisms ⋮ Unnamed Item

Uses Software

• Coq
• Twelf
• Automath
• PoplMark
• Nominal Isabelle

Cites Work

• Unnamed Item
• Unnamed Item
• Nominal techniques in Isabelle/HOL
• Nominal logic, a first order theory of names and binding
• Some lambda calculus and type theory formalized
• A canonical locally named representation of binding
• Engineering formal metatheory
• A framework for defining logics
• F-ing modules
• Theorem Proving in Higher Order Logics

This page was built for publication: Mechanizing metatheory without typing contexts