Zobrazeno 1 - 10
of 64
pro vyhledávání: '"Norrish, A."'
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:
Norma Norrish
Publikováno v:
IALLT Journal of Language Learning Technologies. 10:67-72
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:
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
Autor:
Michael Norrish, Yong Kiam Tan, Oskar Abrahamsson, Magnus O. Myreen, Andreas Lööw, Ramana Kumar, Anthony Fox
Publikováno v:
PLDI
Developing technology for building verified stacks, i.e., computer systems with comprehensive proofs of correctness, is one way the science of programming languages furthers the computing discipline. While there have been successful projects verifyin
The CakeML compiler is, to the best of our knowledge, the most realistic verified compiler for a functional programming language to date. The architecture of the compiler, a sequence of intermediate languages through which high-level features are com
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::a2340d573dc0090ba0aa1f97cd38eebc
https://kar.kent.ac.uk/71304/1/paper.pdf
https://kar.kent.ac.uk/71304/1/paper.pdf
Autor:
Matthew Fairbairn, Hannes Mehnert, Tom Ridge, Michael J. A. Smith, Peter Sewell, Michael Norrish, Steve Bishop, Keith Wansbrough
Conventional computer engineering relies on test-and-debug development processes, with the behavior of common interfaces described (at best) with prose specification documents. But prose specifications cannot be used in test-and-debug development in
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::e46bdb0f32d4e913906cbc78c2fd2b71