Browse by Person (creator, editor, contributor, etc.)
 | Up a level |
Number of items: 10.
Article
| Tan, Yong Kiam and Myreen, Magnus O. and Kumar, Ramana and Fox, Anthony and Owens, Scott and Norrish, Michael (2019) The Verified CakeML Compiler Backend. Journal of Functional Programming, 29 . ISSN 0956-7968. (doi:https://doi.org/10.1017/S0956796818000229) (Access to this publication is currently restricted. You may be able to access a copy if URLs are provided) |
![[img]](https://kar.kent.ac.uk/style/images/fileicons/application_pdf.png)
|
| Owens, Scott and Norrish, Michael and Kumar, Ramana and Myreen, Magnus O. and Tan, Yong Kiam (2017) Verifying Efficient Function Calls in CakeML. Proceedings of the ACM Programming Languages, 1 (ICFP). ISSN 2475-1421. E-ISSN 2475-1421. (doi:https://doi.org/10.1145/3110262) (Full text available) |
|
| Kumar, Ramana and Arthan, Rob and Myreen, Magnus O. and Owens, Scott (2016) Self-Formalisation of Higher-Order Logic: Semantics, Soundness, and a Verified Implementation. Journal of Automated Reasoning, 56 (3). pp. 221-259. ISSN 0168-7433. E-ISSN 1573-0670. (doi:https://doi.org/10.1007/s10817-015-9357-x) (Access to this publication is currently restricted. You may be able to access a copy if URLs are provided) |
|
Book section
| Férée, Hugo and Pohjola, Johannes Aman and Kumar, Ramana and Owens, Scott and Myreen, Magnus O. and Ho, Son (2018) Program Verification in the Presence of I/O. In: Verified Software. Theories, Tools, and Experiments. Lecture Notes in Computer Science . Springer. ISBN 978-3-030-03591-4. (doi:https://doi.org/10.1007/978-3-030-03592-1_6) (Full text available) |
|
| Myreen, Magnus O. and Owens, Scott and Kumar, Ramana (2013) Steps Towards Verified Implementations of HOL Light (Rough Diamond). In: Interactive Theorem Proving 4th International Conference. Lecture Notes in Computer Science . Springer, Berlin, Germany, pp. 490-495. ISBN 978-3-642-39633-5. E-ISBN 978-3-642-39634-2. (doi:https://doi.org/10.1007/978-3-642-39634-2_38) (The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided) |
Conference or workshop item
| Tan, Yong Kiam and Myreen, Magnus O. and Kumar, Ramana and Fox, Anthony and Owens, Scott and Norrish, Michael (2016) A New Verified Compiler Backend for CakeML. In: International Conference on Functional Programming, Sep 2016, Nara, Japan. (doi:https://doi.org/10.1145/2951913.2951924) (Full text available) |
|
| Owens, Scott and Myreen, Magnus O. and Kumar, Ramana and Tan, Yong Kiam (2016) Functional Big-step Semantics. In: Lecture Notes in Computer Science. Lecture Notes in Computer Science. Springer (doi:https://doi.org/10.1007/978-3-662-49498-1_23) (Full text available) |
|
| Tan, Yong Kiam and Owens, Scott and Kumar, Ramana (2015) A Verified Type System for CakeML. In: Implementation and application of functional programming languages, 14-16 September, 2015, Koblenz, Germany. (doi:https://doi.org/10.1145/2897336.2897344) (Full text available) |
|
| Kumar, Ramana and Arthan, Rob and Myreen, Magnus O. and Owens, Scott (2014) HOL with Definitions: Semantics, Soundness, and a Verified Implementation. In: Interactive Theorem Proving: Fifth International Conference, ITP 2014. Lecture Notes in Computer Science, 8558. Springer pp. 308-324. (doi:https://doi.org/10.1007/978-3-319-08970-6_20) (Full text available) |
|
| Kumar, Ramana and Myreen, Magnus O. and Norrish, Michael and Owens, Scott (2014) CakeML: A Verified Implementation of ML. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press pp. 179-191. ISBN 978-1-4503-2544-8. (doi:https://doi.org/10.1145/2535838.2535841) (The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided) |
