Zobrazeno 1 - 10
of 70
pro vyhledávání: '"Michael Norrish"'
Autor:
Hing Lun Chan, Michael Norrish
Publikováno v:
Journal of Formalized Reasoning, Vol 6, Iss 1, Pp 63-87 (2013)
We discuss mechanised proofs of Fermat's Little Theorem in a variety of styles, focusing in particular on an elegant combinatorial ``necklace'' proof that has not been mechanised previously.What is elegant in prose turns out to be long-winded mechani
Externí odkaz:
https://doaj.org/article/c585e2e2e6ae41489a10fcf0369be5b6
Autor:
Michael Norrish, Hing Lun Chan
Publikováno v:
Journal of Automated Reasoning. 65:205-256
The AKS algorithm (by Agrawal, Kayal and Saxena) is a significant theoretical result, establishing “PRIMES in P” by a brilliant application of ideas from finite fields. This paper describes an implementation of the AKS algorithm in our theorem pr
Publikováno v:
Journal of Automated Reasoning
We implement a automated tactical prover TacticToe on top of the HOL4 interactive theorem prover. TacticToe learns from human proofs which mathematical technique is suitable in each proof situation. This knowledge is then used in a Monte Carlo tree s
Autor:
Magnus O. Myreen, Michael Norrish, Son Ho, Hrutvik Kanabar, Yong Kiam Tan, Ramana Kumar, Oskar Abrahamsson
Publikováno v:
Journal of Automated Reasoning. 64:1287-1306
We introduce an automatic method for producing stateful ML programs together with proofs of correctness from monadic functions in HOL. Our mechanism supports references, exceptions, and I/O operations, and can generate functions manipulating local st
Autor:
Hing-Lun Chan, Michael Norrish
Publikováno v:
Journal of Automated Reasoning. 63:667-693
We present a formalisation of the theory of finite fields, from basic axioms to their classification, both existence and uniqueness, in HOL4 using the notion of subfields. The tools developed are applied to the characterisation of subfields of finite
Autor:
Elliot Catt, Michael Norrish
Publikováno v:
CPP
Kolmogorov complexity is an essential tool in the study of algorithmic information theory, and is used in the fields of Artificial Intelligence, cryptography, and coding theory. The formalisation of the theorems of Kolmogorov complexity is also key t
Publikováno v:
VMIL@SPLASH
Applications of real-time systems have grown significantly in both diversity and popularity, and the appetite for real-time software has never been higher. In contrast, the choice of programming languages used to develop such systems has stagnated, m
Publikováno v:
Journal of Automated Reasoning. 61:485-520
A completeness threshold is required to guarantee the completeness of planning as satisfiability, and bounded model checking of safety properties. We investigate completeness thresholds related to the diameter of the underlying transition system. A v
Publikováno v:
Proceedings of the ACM on Programming Languages. 1:1-27
We have designed an intermediate language (IL) for the CakeML compiler that supports the verified, efficient compilation of functions and calls. Verified compilation steps include batching of multiple curried arguments, detecting calls to statically
Publikováno v:
Proceedings of the International Conference on Automated Planning and Scheduling. 27:2-10
We investigate compositional bounding of transition system diameters, with application in bounding the lengths of plans. We establish usefully-tight bounds by exploiting acyclicity in state-spaces. We provide mechanised proofs in HOL4 of the validity