James Power - Papers Published in 1999

This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.

Working with Linear Logic in Coq

James Power and Caroline Webster,
12th International Conference on Theorem Proving in Higher Order Logics (Work-in-progress paper),
University of Nice, France, September 14-17, 1999.

In this paper we describe the encoding of linear logic in the Coq system, a proof assistant for higher-order logic. This process involved encoding a suitable consequence relation, the relevant operators, and some auxiliary theorems and tactics. The encoding allows us to state and prove theorems in linear logic, and we demonstrate its use through two examples: a simple blocks world scenario, and the Towers of Hanoi problem.

Four Logics and a Protocol

David Gray, Geoff Hamilton, David Sinclair, Paul Gibson and James Power,
3rd. Irish Workshop in Formal Methods,
National University of Ireland, Galway, Ireland, July 1-2, 1999.

The Internet Protocol (IP) is the protocol used to provide connectionless communication between hosts connected to the Internet. It provides a basic internetworking service to transport protocols such as Transmission Control Protocol (TCP) and User Datagram Protocol (UDP). These in turn provide both connection-oriented and connectionless services to applications such as file transfer (FTP) and WWW browsing. In this paper we present four separate specifications of the interface to the internetworking layer implemented by IP using four types of logic: classical, constructive, temporal and linear logic.

Contact: James Power
Last revised: {$todays_date}