Structuring metatheory on inductive definitions

DOI10.1006/INCO.2000.2858zbMath1005.03008OpenAlexW2091186628MaRDI QIDQ1854368

Seán Matthews, David A. Basin

Publication date: 14 January 2003

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1006/inco.2000.2858

zbMATH Keywords

modal logicdeduction theoremmachine-supported metatheory

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (1)

Let’s Get Physical: Models and Methods for Real-World Security Protocols

Uses Software

• Isabelle
• ML
• Isabelle/ZF
• HOL
• Nuprl
• LCF

Cites Work

• Using typed lambda calculus to implement formal systems on a machine
• Isabelle. A generic theorem prover
• Edinburgh LCF. A mechanized logic of computation
• Set theory for verification. II: Induction and recursion
• A fixedpoint approach to implementing (Co)inductive definitions
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Structuring metatheory on inductive definitions