Embedding programming logics in hol theorem prover
by A. Azurat, I.S.W.B. Prasetya, S.D. Swierstra ([Publisher not identified]
, 2002)
|
HOL is a theorem prover based on a higher order logic. Its expressive logic makes it suitable for embedding programming logics. Compared to other theorem provers, HOL is attractive because of its familiar and intuitive logic and because it is highly programmable. In this paper we will compare a number of commonly used embedding approaches in HOL and outline their strength and weakness. We will also outline a new alternative called hybrid embedding that combines the strength of other approaches, though some price will have to be paid. |
|
No. Panggil : | JIKT-2-1-Mei2002-18 |
Entri utama-Nama orang : | |
Entri tambahan-Nama orang : | |
Penerbitan : | [Place of publication not identified]: [Publisher not identified], 2002 |
Sumber Pengatalogan : | |
ISSN : | |
Majalah/Jurnal : | Jurnal Ilmu Komputer dan Teknologi Informasi |
Volume : | Vol. 2 (1) Mei2002: 19-24 |
Tipe Konten : | text |
Tipe Media : | computer |
Tipe Carrier : | online resource |
Akses Elektronik : | |
Institusi Pemilik : | Universitas Indonesia |
Lokasi : |
No. Panggil | No. Barkod | Ketersediaan |
---|---|---|
JIKT-2-1-Mei2002-18 | 03-20-852497588 | TERSEDIA |
Ulasan: |
Tidak ada ulasan pada koleksi ini: 90409 |