Type-omega DPLs
Type-omega DPLs (Denotational Proof Languages) are languages for proof presentation and search that offer strong soundness guarantees. LCF-type systems such as HOL offer similar guarantees, but their soundness relies heavily on static type systems. By contrast, DPLs ensure soundness dynamically, th...
Main Author: | Arkoudas, Konstantine |
---|---|
Language: | en_US |
Published: |
2004
|
Subjects: | |
Online Access: | http://hdl.handle.net/1721.1/6662 |
Similar Items
-
Type-alpha DPLs
by: Arkoudas, Konstantine
Published: (2004) -
Simplifying transformations for type-alpha certificates
by: Arkoudas, Konstantine
Published: (2004) -
Structural Rules in Natural Deduction with Alternatives
by: Greg Restall
Published: (2023-06-01) -
The Faithfulness Problem
by: Mario Bacelar Valente
Published: (2022-12-01) -
Labelled Natural Deduction for Public Announcement Logic with Common Knowledge
by: Muhammad Farhan Mohd Nasir, et al.
Published: (2020-04-01)