HOL

HOL
Tekijä fi: Michael JC Gordon
Tiedostotunniste _ .sml
Lisenssi Muokattu (3-lauseke) BSD-lisenssi
Verkkosivusto hol-theorem-prover.org

HOL (Higher Order Logic)  on vuorovaikutteisen lauseen todistamisen työkaluperhe, joka luotiin käyttämällä samanlaisia ​​lähestymistapoja korkeamman asteen logiikkaan perustuvien todisteiden rakentamiseen ja samanlaisia ​​toteutustapoja. HOL kehittää LCF - järjestelmälähestymistapaa .

Toteutuslogiikka

Valitut projektit HOL:lla

Todisteet muodollisesta oikeellisuudesta kehitettiin CakeML-projektilla [1]  , joka on muodollisesti määritelty ja varmennettu versio ML-kielestä . Ennen tätä HOL:ia käytettiin toteuttamaan muodollisesti määritelty ja varmennettu LISP -versio, joka toimi ARM-, x86- ja PowerPC-prosessoreilla [2] .

HOL:ia on myös käytetty muotosemantiikan kehittämiseen x86-moniprosessorivariantille [3] sekä Power ISA- ja ARM-käskyjoukkojen formaalisen semantiikan määrittelyyn [4] .

Kirjallisuus

Linkit

Muistiinpanot

  1. ↑ CakeML . Haettu 25. marraskuuta 2020. Arkistoitu alkuperäisestä 14. syyskuuta 2020.
  2. ↑ Magnus O. Myreen; Michael JC Gordon. Vahvistetut LISP-toteutukset ARM-, x86- ja PowerPC-järjestelmissä (PDF) . TPHOLs 2009.pp. 359-374. Arkistoitu alkuperäisestä (PDF) 2020-11-09 . Haettu 25.11.2020 . Käytöstä poistettu parametri |deadlink=( ohje )
  3. ↑ Peter Sewell; Sumit Sarkar; Scott Owens; Francesco Zappa Nardelli; Magnus O. Myreen (2010). “x86-TSO: tiukka ja käyttökelpoinen ohjelmoijamalli x86-moniprosessoreille” (PDF) . ACM:n viestintä . 53 (7): 89-97. DOI : 10.1145/1785414.1785443 . Arkistoitu (PDF) alkuperäisestä 30.11.2020 . Haettu 25.11.2020 . Käytöstä poistettu parametri |deadlink=( ohje )
  4. ↑ Jade Alglave; Anthony CJ Fox; Samin Ishtiaq; Magnus O. Myreen; Sumit Sarkar; Peter Sewell; Francesco Zappa Nardelli. Tehon ja ARM-moniprosessorikonekoodin semantiikka (PDF) . KOSTE 2009.s. 13-24. Arkistoitu alkuperäisestä (PDF) 2020-09-19 . Haettu 25.11.2020 . Käytöstä poistettu parametri |deadlink=( ohje )