Trends in Functional Programming
18th International Symposium, TFP 2017, Canterbury, UK, June 19-21, 2017, Revised Selected Papers
Page
%P
-
Chapter and Conference Paper
Modular Relaxed Dependencies in Weak Memory Concurrency
We present a denotational semantics for weak memory concurrency that avoids thin-air reads, provides data-race free programs with sequentially consistent semantics (DRF-SC), and supports a compositional refinemen...
-
Book and Conference Proceedings
-
Chapter and Conference Paper
Program Verification in the Presence of I/O
Software verification tools that build machine-checked proofs of functional correctness usually focus on the algorithmic content of the code. Their proofs are not grounded in a formal semantic model of the env...
-
Article
Open AccessSelf-Formalisation of Higher-Order Logic
We present a mechanised semantics for higher-order logic (HOL), and a proof of soundness for the inference system, including the rules for making definitions, implemented by the kernel of the HOL Light theorem...
-
Chapter and Conference Paper
A High-Assurance, High-Performance Hardware-Based Cross-Domain System
Guardol is a domain-specific language focused on the creation of high-assurance cross-domain systems (i.e., network guards). The Guardol system generates executable code from Guardol programs while also providing...
-
Chapter and Conference Paper
Functional Big-Step Semantics
When doing an interactive proof about a piece of software, it is important that the underlying programming language’s semantics does not make the proof unnecessarily difficult or unwieldy. Both small-step and ...
-
Article
Childhood Obesity and the Metabolic Syndrome
Although research published during the past year suggests the prevalence of childhood obesity in the USA may have plateaued, it remains unacceptably high and places large numbers of youths at elevated risk of ...
-
Article
Physical Activity and Cardiometabolic Biomarkers in Youths: A 2013 Update
Our understanding of the relationships between cardiometabolic risk factors in young people and lifestyle, physiology and genetics continues to grow. This review examines research published during the past 12 ...
-
Chapter and Conference Paper
HOL with Definitions: Semantics, Soundness, and a Verified Implementation
We present a mechanised semantics and soundness proof for the HOL Light kernel including its definitional principles, extending Harrison’s verification of the kernel without definitions. Soundness of the logic...
-
Chapter and Conference Paper
Steps towards Verified Implementations of HOL Light
This short paper describes our plans and progress towards construction of verified ML implementations of HOL Light: the first formally proved soundness result for an LCF-style prover. Building on Harrison’s fo...
-
Chapter and Conference Paper
An Axiomatic Memory Model for POWER Multiprocessors
The growing complexity of hardware optimizations employed by multiprocessors leads to subtle distinctions among allowed and disallowed behaviors, posing challenges in specifying their memory models formally an...
-
Chapter and Conference Paper
Lem: A Lightweight Tool for Heavyweight Semantics
Many ITP developments exist in the context of a single prover, and are dominated by proof effort. In contrast, when applying rigorous semantic techniques to realistic computer systems, engineering the definiti...
-
Chapter
Compiling Higher Order Logic by Proof
We discuss the front end of a compiler whose source language is a subset of higher order logic. The compiler operates by a series of source-to-source transformations in which each transformation step performs ...
-
Chapter and Conference Paper
Reasoning about the Implementation of Concurrency Abstractions on x86-TSO
With the rise of multi-core processors, shared-memory concurrency has become a widespread feature of computation, from hardware, to operating systems, to programming languages such as C++ and Java. However, no...
-
Chapter and Conference Paper
A Better x86 Memory Model: x86-TSO
Real multiprocessors do not provide the sequentially consistent memory that is assumed by most work on semantics and verification. Instead, they have relaxed memory models, typically described in ambiguous pro...
-
Article
Adapting functional programs to higher order logic
Higher-order logic proof systems combine functional programming with logic, providing functional programmers with a comfortable setting for the formalization of programs, specifications, and proofs. However, a...
-
Chapter and Conference Paper
A Sound Semantics for OCaml light
Few programming languages have a mathematically rigorous definition or metatheory—in part because they are perceived as too large and complex to work with. This paper demonstrates the feasibility of such under...
-
Article
Proof producing synthesis of arithmetic and cryptographic hardware
A compiler from a synthesisable subset of higher order logic to clocked synchronous hardware is described. It is being used to create coprocessors for cryptographic and arithmetic applications. The compiler au...
-
Chapter and Conference Paper
Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic
We give an overview of a proof-producing compiler which translates recursion equations, defined in higher order logic, to assembly language. The compiler is implemented and validated with a mix of translation ...
-
Chapter and Conference Paper
Syntactic Abstraction in Component Interfaces
In this paper, we show how to combine a component system and a macro system. A component system separates the definition of a program fragment from the statements that link it, enabling independent compilation...
