|
Working with Linear Logic in CoqJames 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 ProtocolDavid 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.
|