A natural deduction approach to dynamic logic

DOI10.1007/3-540-61780-9_69zbMath1434.03084OpenAlexW1555705349MaRDI QIDQ4647578

Furio Honsell, Marino Miculan

Publication date: 15 January 2019

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/11390/682297

zbMATH Keywords

natural deductiontype theorylogical frameworkproof systemprogram logic

Mathematics Subject Classification ID

Other nonclassical logic (03B60) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (4)

Mechanizing type environments in weak HOAS ⋮ Unnamed Item ⋮ \(\pi\)-calculus in (Co)inductive-type theory ⋮ On the formalization of the modal \(\mu\)-calculus in the calculus of inductive constructions

Uses Software

• Coq
• LEGO
• Elf

Cites Work

• Using typed lambda calculus to implement formal systems on a machine
• Simple consequence relations
• The calculus of constructions
• Encoding modal logics in logical frameworks
• Ten Years of Hoare's Logic: A Survey—Part I
• Axiomatic Definitions of Programming Languages
• A framework for defining logics
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A natural deduction approach to dynamic logic