The Coq mailing list

[satrajit AT attbi.com]

Where can I learn about converting TLA+ syntax used 
in 'Specifying Systems' by Leslie Lamport to Coq?

I assume it should be possible to do so. Is my 
assumption correct?

Here is a simple example of TLA+ specification for an 
asynchronous interface:

------------------ MODULE AsynchInterface --------------
-------
EXTENDS Naturals
CONSTANT Data
VARIABLES val, rdy, ack

TypeInvariant == /\ val \in Data
                 /\ rdy \in {0, 1}
                 /\ ack \in {0, 1}
--------------------------------------------------------
-----
Init == /\ val \in Data
        /\ rdy \in {0, 1}
        /\ ack = rdy

Send == /\ rdy = ack
        /\ val' \in Data
        /\ rdy' = 1 - rdy
        /\ UNCHANGED ack

Rcv  == /\ rdy # ack
        /\ ack' = 1 - ack
        /\ UNCHANGED <<val, rdy>>

Next == Send \/ Rcv

Spec == Init /\ [][Next]_<<val, rdy, ack>>

--------------------------------------------------------
------
THEOREM Spec => []TypeInvariant
========================================================
======