ORCID Profile
0000-0002-6406-7875
Current Organisation
UNSW Sydney
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.
Publisher: Springer International Publishing
Date: 2019
Publisher: EasyChair
DOI: 10.29007/413D
Abstract: Isabelle/HOL augments classical higher-order logic with ad-hoc overloading of constant definitions— that is, one constant may have several definitions for non-overlapping types. In this paper, we present a mechanised proof that HOL with ad-hoc overloading is consistent. All our results have been formalised in the HOL4 theorem prover.
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 Berlin Heidelberg
Date: 2016
Publisher: Springer Berlin Heidelberg
Date: 2011
Publisher: Springer Science and Business Media LLC
Date: 03-11-2018
Publisher: Centre pour la Communication Scientifique Directe (CCSD)
Date: 31-03-2016
Abstract: Applied process calculi include advanced programming constructs such as type systems, communication with pattern matching, encryption primitives, concurrent constraints, nondeterminism, process creation, and dynamic connection topologies. Several such formalisms, e.g. the applied pi calculus, are extensions of the the pi-calculus a growing number is geared towards particular applications or computational paradigms. Our goal is a unified framework to represent different process calculi and notions of computation. To this end, we extend our previous work on psi-calculi with novel abstract patterns and pattern matching, and add sorts to the data term language, giving sufficient criteria for subject reduction to hold. Our framework can directly represent several existing process calculi the resulting transition systems are isomorphic to the originals up to strong bisimulation. We also demonstrate different notions of computation on data terms, including cryptographic primitives and a lambda-calculus with erratic choice. Finally, we prove standard congruence and structural properties of bisimulation the proof has been machine-checked using Nominal Isabelle in the case of a single name sort.
Publisher: Open Publishing Association
Date: 12-01-2021
DOI: 10.4204/EPTCS.332.1
Publisher: Association for Computing Machinery (ACM)
Date: 13-11-2020
DOI: 10.1145/3428272
Abstract: Garbage collectors relieve the programmer from manual memory management, but lead to compiler-generated machine code that can behave differently (e.g. out-of-memory errors) from the source code. To ensure that the generated code behaves exactly like the source code, programmers need a way to answer questions of the form: what is a sufficient amount of memory for my program to never reach an out-of-memory error? This paper develops a cost semantics that can answer such questions for CakeML programs. The work described in this paper is the first to be able to answer such questions with proofs in the context of a language that depends on garbage collection. We demonstrate that positive answers can be used to transfer liveness results proved for the source code to liveness guarantees about the generated machine code. Without guarantees about space usage, only safety results can be transferred from source to machine code. Our cost semantics is phrased in terms of an abstract intermediate language of the CakeML compiler, but results proved at that level map directly to the space cost of the compiler-generated machine code. All of the work described in this paper has been developed in the HOL4 theorem prover.
Publisher: Open Publishing Association
Date: 06-08-2014
DOI: 10.4204/EPTCS.160.2
Publisher: Cambridge University Press (CUP)
Date: 24-06-2013
DOI: 10.1017/S0960129513000170
Abstract: In earlier work we explored the expressiveness and algebraic theory Psi-calculi, which form a parametric framework for extensions of the pi-calculus. In the current paper we consider higher-order psi-calculi through a technically surprisingly simple extension of the framework, and show how an arbitrary psi-calculus can be lifted to its higher-order counterpart in a canonical way. We illustrate this with ex les and establish an algebraic theory of higher-order psi-calculi. The formal results are obtained by extending our proof repositories in Isabelle/Nominal.
Publisher: Springer International Publishing
Date: 2014
Publisher: Springer International Publishing
Date: 2018
Publisher: Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH, Wadern/Saarbruecken, Germany
Date: 2019
Publisher: Springer International Publishing
Date: 2018
Publisher: Springer Science and Business Media LLC
Date: 08-11-2013
Publisher: Springer International Publishing
Date: 2017
Publisher: ACM
Date: 18-01-2016
Publisher: Springer International Publishing
Date: 2014
Publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
Date: 2022
Publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
Date: 2022
Publisher: episciences.org
Date: 2020
No related grants have been discovered for Johannes Åman Pohjola.