The Coq mailing list

[Wojciech Jedynak <wjedynak AT gmail.com>]

Dear Coq community,

during my master studies I have worked on the formal semantics of
Ltac. The dissertation is now finished and you can find it at
[http://www.ii.uni.wroc.pl/~wjedynak/publications/master.pdf]
The semantics of Ltac is presented in an incremental way starting from
tactics ala LCF and
some other aspects of a proof engine (the proof shell and simplified
atomic tactics) are studied,
so I hope the dissertation could be useful as a rigorous documentation
for the users.

If you are only interested in the final semantics, then please take a
look at the corresponding paper (written together with M. Biernacka
and D. Biernacki), available at
[http://www.ii.uni.wroc.pl/~wjedynak/publications/jedynak-al-ppdp13.pdf]

Best regards,
Wojciech Jedynak