CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Self-Formalisation of Higher-Order Logic Semantics, Soundness, and a Verified Implementation

R. Kumar ; R. Arthan ; Magnus Myreen (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; S. Owens
Journal of Automated Reasoning (0168-7433). Vol. 56 (2016), 3, p. 221-259.
[Artikel, refereegranskad vetenskaplig]

We present a mechanised semantics for higher-order logic (HOL), and a proof of soundness for the inference system, including the rules for making definitions, implemented by the kernel of the HOL Light theorem prover. Our work extends Harrison's verification of the inference system without definitions. Soundness of the logic extends to soundness of a theorem prover, because we also show that a synthesised implementation of the kernel in CakeML refines the inference system. Apart from adding support for definitions and synthesising an implementation, we improve on Harrison's work by making our model of HOL parametric on the universe of sets, and we prove soundness for an improved principle of constant specification in the hope of encouraging its adoption. Our semantics supports defined constants directly via a context, and we find this approach cleaner than our previous work formalising Wiedijk's Stateless HOL.

Nyckelord: HOL, Higher-order logic, Verification, Interactive theorem proving, Theorem proving, Consistency



Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2016-04-15. Senast ändrad 2016-09-09.
CPL Pubid: 234751

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)