ORCID Profile
0000-0003-1163-8467
Current Organisation
Australian National University
Does something not look right? The information on this page has been harvested from data sources that may not be up to date. We continue to work with information providers to improve coverage and quality. To report an issue, use the Feedback Form.
In Research Link Australia (RLA), "Research Topics" refer to ANZSRC FOR and SEO codes. These topics are either sourced from ANZSRC FOR and SEO codes listed in researchers' related grants or generated by a large language model (LLM) based on their publications.
Programming Languages | Computer Software | Computer System Security | Concurrent Programming
Expanding Knowledge in the Information and Computing Sciences | Application Tools and System Utilities |
Publisher: Springer Berlin Heidelberg
Date: 2011
Publisher: Association for Computing Machinery (ACM)
Date: 06-06-2023
DOI: 10.1145/3591259
Abstract: We present PureCake, a mechanically-verified compiler for PureLang, a lazy, purely functional programming language with monadic effects. PureLang syntax is Haskell-like and indentation-sensitive, and its constraint-based Hindley-Milner type system guarantees safe execution. We derive sound equational reasoning principles over its operational semantics, dramatically simplifying some proofs. We prove end-to-end correctness for the compilation of PureLang down to machine code---the first such result for any lazy language---by targeting CakeML and composing with its verified compiler. Multiple optimisation passes are necessary to handle realistic lazy idioms effectively. We develop PureCake entirely within the HOL4 interactive theorem prover.
Publisher: Springer Science and Business Media LLC
Date: 02-09-2020
Publisher: Springer Berlin Heidelberg
Date: 2013
Publisher: ACM
Date: 25-03-2018
Publisher: Springer Berlin Heidelberg
Date: 2009
Publisher: ACM
Date: 04-09-2016
Publisher: Association for Computing Machinery (ACM)
Date: 29-08-2017
DOI: 10.1145/3110262
Abstract: 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 known functions, and specialising calls to known functions with no free variables. Finally, we verify the translation to a lower-level IL that only supports closed, first-order functions. These compilation steps resemble those found in other compilers (especially OCaml). Our contribution here is the design of the semantics of the IL, and the demonstration that our verification techniques over this semantics work well in practice at this scale. The entire development was carried out in the HOL4 theorem prover.
Publisher: ACM
Date: 17-01-2021
Publisher: Association for Computing Machinery (ACM)
Date: 12-12-2018
DOI: 10.1145/3243650
Abstract: 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 any automated way, and prose is a poor medium for expressing complex (and loose) specifications. The TCP/IP protocols and Sockets API are a good ex le of this: they play a vital role in modern communication and computation, and interoperability between implementations is essential. But what exactly they are is surprisingly obscure: their original development focused on “rough consensus and running code,” augmented by prose RFC specifications that do not precisely define what it means for an implementation to be correct. Ultimately, the actual standard is the de facto one of the common implementations, including, for ex le, the 15 000 to 20 000 lines of the BSD implementation—optimized and multithreaded C code, time dependent, with asynchronous event handlers, intertwined with the operating system, and security critical. This article reports on work done in the Netsem project to develop lightweight mathematically rigorous techniques that can be applied to such systems: to specify their behavior precisely (but loosely enough to permit the required implementation variation) and to test whether these specifications and the implementations correspond with specifications that are executable as test oracles . We developed post hoc specifications of TCP, UDP, and the Sockets API, both of the service that they provide to applications (in terms of TCP bidirectional stream connections) and of the internal operation of the protocol (in terms of TCP segments and UDP datagrams), together with a testable abstraction function relating the two. These specifications are rigorous, detailed, readable, with broad coverage, and rather accurate. Working within a general-purpose proof assistant (HOL4), we developed language idioms (within higher-order logic) in which to write the specifications: operational semantics with nondeterminism, time, system calls, monadic relational programming, and so forth. We followed an experimental semantics approach, validating the specifications against several thousand traces captured from three implementations (FreeBSD, Linux, and WinXP). Many differences between these were identified, as were a number of bugs. Validation was done using a special-purpose symbolic model checker programmed above HOL4. Having demonstrated that our logic-based engineering techniques suffice for handling real-world protocols, we argue that similar techniques could be applied to future critical software infrastructure at design time, leading to cleaner designs and (via specification-based testing) more robust and predictable implementations. In cases where specification looseness can be controlled, this should be possible with lightweight techniques, without the need for a general-purpose proof assistant, at relatively little cost.
Publisher: Springer Science and Business Media LLC
Date: 31-07-2009
Publisher: Springer International Publishing
Date: 2018
Publisher: ACM
Date: 14-06-2016
Publisher: Springer International Publishing
Date: 2020
Publisher: Springer International Publishing
Date: 2018
Publisher: Springer Berlin Heidelberg
Date: 1999
Publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
Date: 2022
Publisher: Springer Science and Business Media LLC
Date: 25-10-2018
Publisher: Cambridge University Press (CUP)
Date: 2019
DOI: 10.1017/S0956796818000229
Abstract: 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 compiled away incrementally, enables verification of each compilation pass at an appropriate level of semantic detail. Parts of the compiler’s implementation resemble mainstream (unverified) compilers for strict functional languages, and it supports several important features and optimisations. These include efficient curried multi-argument functions, configurable data representations, efficient exceptions, register allocation, and more. The compiler produces machine code for five architectures: x86-64, ARMv6, ARMv8, MIPS-64, and RISC-V. The generated machine code contains the verified runtime system which includes a verified generational copying garbage collector and a verified arbitrary precision arithmetic (bignum) library. In this paper, we present the overall design of the compiler backend, including its 12 intermediate languages. We explain how the semantics and proofs fit together and provide detail on how the compiler has been bootstrapped inside the logic of a theorem prover. The entire development has been carried out within the HOL4 theorem prover.
Publisher: Springer Berlin Heidelberg
Date: 2004
Publisher: ACM
Date: 22-08-2005
Publisher: Springer International Publishing
Date: 2015
Publisher: ACM
Date: 11-07-2021
Publisher: Springer Berlin Heidelberg
Date: 2017
Publisher: Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH, Wadern/Saarbruecken, Germany
Date: 2015
Publisher: Association for Computing Machinery (ACM)
Date: 06-2010
Publisher: Springer International Publishing
Date: 2018
Publisher: ACM
Date: 08-06-2019
Publisher: Springer Science and Business Media LLC
Date: 02-03-2011
Publisher: Springer Science and Business Media LLC
Date: 14-10-2017
Location: United Kingdom of Great Britain and Northern Ireland
Start Date: 06-2019
End Date: 12-2024
Amount: $480,000.00
Funder: Australian Research Council
View Funded Activity