Home
Journals
Archaeology International
Architecture_MPS
Europe and the World: A law review
Film Education Journal
History Education Research Journal
International Journal of Development Education and Global Learning
International Journal of Social Pedagogy
Jewish Historical Studies: A Journal of English-Speaking Jewry
Journal of Bentham Studies
London Review of Education
Radical Americas
Research for All
The Journal of the Sylvia Townsend Warner Society
The London Journal of Canadian Studies
About
About UCL Press
Who we are
Contact us
My ScienceOpen
Sign in
Register
Dashboard
Search
Home
Journals
Archaeology International
Architecture_MPS
Europe and the World: A law review
Film Education Journal
History Education Research Journal
International Journal of Development Education and Global Learning
International Journal of Social Pedagogy
Jewish Historical Studies: A Journal of English-Speaking Jewry
Journal of Bentham Studies
London Review of Education
Radical Americas
Research for All
The Journal of the Sylvia Townsend Warner Society
The London Journal of Canadian Studies
About
About UCL Press
Who we are
Contact us
My ScienceOpen
Sign in
Register
Dashboard
Search
38
views
15
references
Top references
cited by
1
Cite as...
0 reviews
Review
0
comments
Comment
0
recommends
+1
Recommend
0
collections
Add to
0
shares
Share
Twitter
Sina Weibo
Facebook
Email
2,895
similar
All similar
Record
: found
Abstract
: not found
Book Chapter
: not found
Sharing HOL4 and HOL Light Proof Knowledge
other
Author(s):
Thibault Gauthier
,
Cezary Kaliszyk
Publication date
(Online):
November 22 2015
Publisher:
Springer Berlin Heidelberg
Read this book at
Publisher
Buy book
Review
Review book
Invite someone to review
Bookmark
Cite as...
There is no author summary for this book yet. Authors can add summaries to their books on ScienceOpen to make them more accessible to a non-specialist audience.
Related collections
Indigenous Knowledge
Most cited references
15
Record
: found
Abstract
: not found
Article
: not found
Learning-Assisted Automated Reasoning with Flyspeck
Josef Urban
,
Cezary Kaliszyk
(2014)
0
comments
Cited
41
times
– based on
0
reviews
Review now
Bookmark
Record
: found
Abstract
: not found
Book Chapter
: not found
A Brief Overview of HOL4
Konrad Slind
,
Michael Norrish
(2008)
0
comments
Cited
35
times
– based on
0
reviews
Bookmark
Record
: found
Abstract
: not found
Book Chapter
: not found
HOL Light: An Overview
John Harrison
(2009)
0
comments
Cited
22
times
– based on
0
reviews
Bookmark
All references
Author and book information
Book Chapter
Publication date (Print):
2015
Publication date (Online):
November 22 2015
Pages
: 372-386
DOI:
10.1007/978-3-662-48899-7_26
SO-VID:
0c1544b0-a9d7-4a8b-bfad-edc0557c5222
History
Data availability:
Comments
Comment on this book
Sign in to comment
Book chapters
pp. 1
Skolemization for Substructural Logics
pp. 16
Reasoning About Embedded Dependencies Using Inclusion Dependencies
pp. 31
Cobra: A Tool for Solving General Deductive Games
pp. 48
On Anti-subsumptive Knowledge Enforcement
pp. 63
Value Sensitivity and Observable Abstract Values for Information Flow Control
pp. 79
SAT-Based Minimization of Deterministic $$\omega $$ -Automata
pp. 97
Decidability, Introduction Rules and Automata
pp. 112
Analyzing Internet Routing Security Using Model Checking
pp. 130
Boolean Formulas for the Static Identification of Injection Attacks in Java
pp. 178
Automated Benchmarking of Incremental SAT and QBF Solvers
pp. 203
Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs
pp. 219
TIP: Tools for Inductive Provers
pp. 233
Verification of Concurrent Programs Using Trace Abstraction Refinement
pp. 249
Synchronized Recursive Timed Automata
pp. 266
Focused Labeled Proof Systems for Modal Logic
pp. 281
On CTL* with Graded Path Modalities
pp. 297
On Subexponentials, Synthetic Connectives, and Multi-level Delimited Control
pp. 313
On the Expressive Power of Communication Primitives in Parameterised Systems
pp. 329
There Is No Best $$\beta $$ -Normalization Strategy for Higher-Order Reasoners
pp. 340
Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-Vectors
pp. 356
Abstract Domains and Solvers for Sets Reasoning
pp. 372
Sharing HOL4 and HOL Light Proof Knowledge
Similar content
2,895
Effective Normalization Techniques for HOL
Authors:
Max Wisniewski
,
Alexander Steen
,
Kim Kern
…
Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL
Authors:
Sascha Böhme
,
Anthony C. J. Fox
,
Thomas Sewell
…
Linear Programming in Isabelle/HOL
Authors:
Julian Parsert
See all similar
Cited by
1
A Survey of Languages for Formalizing Mathematics
Authors:
Cezary Kaliszyk
,
Florian Rabe
See all cited by