Remember Me
Or use your Academic/Social account:


Or use your Academic/Social account:


You have just completed your registration at OpenAire.

Before you can login to the site, you will need to activate your account. An e-mail will be sent to you with the proper instructions.


Please note that this site is currently undergoing Beta testing.
Any new content you create is not guaranteed to be present to the final version of the site upon release.

Thank you for your patience,
OpenAire Dev Team.

Close This Message


Verify Password:
Verify E-mail:
*All Fields Are Required.
Please Verify You Are Human:
fbtwitterlinkedinvimeoflicker grey 14rssslideshare1
Tan, Yong Kiam; Owens, Scott; Kumar, Ramana
Languages: English
Types: Unknown
Subjects: QA76
CakeML is a dialect of the (strongly typed) ML family of programming\ud languages, designed to play a central role in high-assurance\ud software systems. To date, the main artefact supporting this is a verified\ud compiler from CakeML source code to x86-64 machine code.\ud The verification effort addresses each phase of compilation from\ud parsing through to code generation and garbage collection.\ud In this paper, we focus on the type system: its declarative speci-\ud fication, type soundness theorem, and the soundness and completeness\ud of an implementation of type inference – all formally veri-\ud fied in the HOL4 proof assistant. Each of these aspects of a type\ud system is important in any design and implementation of a typed\ud functional programming language. They allow the programmer to\ud soundly employ (informal) type-based reasoning, and the compiler\ud to apply optimisations that assume type-correctness. So naturally,\ud their verification is a critical part of a verified compiler.
  • The results below are discovered through our pilot algorithms. Let us know how we are doing!

    • [1] L. Damas and R. Milner. Principal type-schemes for functional programs. In Proc. 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '82, pages 207-212. ACM, 1982.
    • [2] D. Dreyer. Understanding and Evolving the ML Module System. PhD thesis, Carnegie Mellon University, 2005.
    • [3] M. Felleisen, R. B. Findler, and M. Flatt. Semantics Engineering with PLT Redex. MIT Press, 2009.
    • [4] R. Harper and M. Lillibridge. A type-theoretic approach to higher-order modules with sharing. In POPL'94: 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 123-137, 1994.
    • [5] R. Kumar, M. O. Myreen, M. Norrish, and S. Owens. CakeML: A verified implementation of ML. In POPL '14: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 179-191. ACM Press, Jan. 2014.
    • [6] R. Kumar and M. Norrish. (Nominal) Unification by recursive descent with triangular substitutions. In Interactive Theorem Proving, First International Conference, ITP 2010, volume 6172 of LNCS, 2010.
    • [7] D. K. Lee, K. Crary, and R. Harper. Towards a mechanized metatheory of Standard ML. In Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '07, pages 173-184. ACM, 2007.
    • [8] X. Leroy. Manifest types, modules, and separate compilation. In POPL'94: 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 109-122, 1994.
    • [9] R. Milner. A theory of type polymorphism in programming. J. Comput. Syst. Sci., 17(3), 1978.
    • [10] R. Milner, M. Tofte, R. Harper, and D. MacQueen. The Definition of Standard ML (Revised). MIT Press, 1997.
    • [11] W. Naraschewski and T. Nipkow. Type inference verified: Algorithm W in Isabelle/HOL. Journal of Automated Reasoning, 23:299-318, 1999.
    • [12] S. Owens. A sound semantics for OCaml light. In Programming Languages and Systems: 17th European Symposium on Programming, ESOP 2008, volume 4960 of LNCS, pages 1- 15. Springer, Mar. 2008.
    • [13] D. Vytiniotis, S. Peyton Jones, and T. Schrijvers. Let should not be generalized. In Proceedings of the 5th ACM SIGPLAN Workshop on Types in Language Design and Implementation, TLDI '10. ACM, 2010.
    • [14] D. Vytiniotis, S. Peyton Jones, T. Schrijvers, and M. Sulzmann. OutsideIn(X) Modular type inference with local assumptions. J. Funct. Program., 21(4-5), 2011.
    • [15] A. K. Wright and M. Felleisen. A syntactic approach to type soundness. Inf. Comput., 115(1):38-94, 1994.
  • No related research data.
  • No similar publications.

Share - Bookmark

Download from

Cite this article