My talk will celebrate Robin Milner's contribution to functional programming via a combination of reminiscences about the early days of ML and speculations about its future.

Realistic formal specifications of machine languages for commercial processors consist of thousands of lines of definitions. Current methods support trustworthy proofs of the correctness of programs for one such specification. However, these methods provide little or no support for reusing proofs of the same algorithm implemented in different machine languages. We describe an approach, based on proof-producing decompilation, which both makes machine-code verification tractable and supports proof reuse between different languages. We briefly present examples based on detailed models of machine code for ARM, PowerPC and x86. The theories and tools have been implemented in the HOL4 system.

Abstract 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 automatically translates a functionfdefined in higher order logic (typically using recursion) into a device that computesfvia a four-phase handshake circuit. Compilation is by fully automatic proof in the HOL4 system, and generates a correctness theorem for each compiled function. Synthesised circuits can be directly translated to Verilog, and then input to design automation tools. A fully-expansive ‘LCF methodology’ allows users to safely modify and extend the compiler’s theorem proving scripts to add optimisations or to enlarge the synthesisable subset of higher order logic.

A link between the ACL2 and HOL4 proof assistants is described. This allows each system to be deployed smoothly within a single formal development. Several applications are being considered: using ACL2's execution environment for simulating HOL models; using ACL2's proof automation to discharge HOL proof obligations; and using HOL to specify and verify properties of ACL2 functions that cannot easily be stated in the first-order ACL2 logic. Care has been taken to ensure sound translations between the logics supported by HOL and ACL2. The initial ACL2 theory has been defined inside HOL, so that it is possible to prove mechanically that first-order ACL2 functions on S-expressions correspond to higher-order functions operating on a variety of types. The translation between the two systems operates at the level of S-expressions and is intended to handle large hardware and software models

Abstract. The Accellera organisation selected Sugar, IBM’s formal specification language, as the basis for a standard to ‘drive assertion-based verification’ in the electronics industry. Sugar combines regular expressions, Linear Temporal Logic (LTL) and Computation Tree Logic (CTL) into a property language intended for both static verification (e.g. model checking) and dynamic verification (e.g. simulation). In 2003 Accellera decided to rename the evolving standard to ‘Accellera Property Specification Language’ (or ‘PSL’ for short). We motivate and describe a deep semantic embedding of PSL in the version of higher-order logic supported by the HOL 4 theorem-proving system. The main goal of this paper is to demonstrate that mechanised theorem proving can be a useful aid to the validation of the semantics of an industrial design language.

Industry standard hardware description languages like Verilog and VHDL are based on event simulation. Formal verification methods such as theorem proving and model checking are based on the analysis of sets of traces of transition systems or automata. There is a semantic gap between these two interpretations and consequently one cannot be sure that results obtained by simulation and formal verification are consistent. This paper is a step towards bridging this gap. A simple simulation cycle is specified for a Verilog-like language and it is shown how for simple examples of practical interest this can be related to a standard formal-verification-oriented model based on traces.

The Verilog hardware description language (HDL) is widely used to model the structure and behaviour of digital systems ranging from simple hardware building blocks to complete systems. Its semantics is based an the scheduling of events and the propagation of changes. Different Verilog models of the same device are used during the design process and it is important that these be 'equivalent'; formal methods for ensuring this could be commercially significant. Unfortunately, there is very little theory available to help. This self-contained tutorial paper explains the semantics of Verilog informally and poses a number of logical and semantic problems that are intended to provoke further research. Any theory developed to support Verilog is likely to be useful for the analysis of the similar (but more complex) language VHDL.

The possibility of extending some of the logical methods that have been recommended for the design of software to the design of hardware, in particular, of synchronous switching circuits implemented in CMOS, is explored. The objective is to design networks that are known by construction. Things that can go wrong with circuits designed in this way are examined. The application of the techniques is discussed.>

The list iteration construct lit is defined by: [equation: see PDF] Many simple list processing functions can be programmed as expressions built up from the LISP primitives (car, cdr, cons,… etc.) and lit, examples include most of the operations of Boolean algebra and primitive recursive arithmetic (with the integer n represented by a list (NIL…:NIL) of n NIL's). This latter example shows that the equivalence of list iteration programs is undecidable. In the paper the use of lit is illustrated and two theorems are proved which exhibit limitations on its power; these enable one to show that, for example, LISP's equal and flatten (where e.g. flatten [(1 (2 3) 4 ((5) 6))] = (1 2 3 4 5 6)) cannot be computed by list iteration alone.

Article Free Access Share on A Metalanguage for interactive proof in LCF Authors: M. Gordon University of Edinburgh University of EdinburghView Profile , R. Milner University of Edinburgh University of EdinburghView Profile , L. Morris Syracuse University Syracuse UniversityView Profile , M. Newey Australian National University Australian National UniversityView Profile , C. Wadsworth University of Edinburgh University of EdinburghView Profile Authors Info & Claims POPL '78: Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languagesJanuary 1978Pages 119–130https://doi.org/10.1145/512760.512773Published:01 January 1978Publication History 55citation684DownloadsMetricsTotal Citations55Total Downloads684Last 12 Months96Last 6 weeks5 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF