coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] are there any formal descriptions of the tatics of Coq?

From: Jonathan Leivent <jonikelee AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] are there any formal descriptions of the tatics of Coq?
Date: Sun, 6 Mar 2016 18:55:24 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f175.google.com
Ironport-phdr: 9a23:tafB/xIBrHDizsqgIdmcpTZWNBhigK39O0sv0rFitYgUKfXxwZ3uMQTl6Ol3ixeRBMOAu60C27Kd6/2ocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TWM5DIfUi/yKRBybrysXNWC0ILnj6vqptX6WEZhunmUWftKNhK4rAHc5IE9oLBJDeIP8CbPuWZCYO9MxGlldhq5lhf44dqsrtY4q3wD86Fpy8kVWqLjOq88ULZwDTI8Mmlz6te4mwPESF6t4X0VTmUflFJsDgnb4RfmFsPztS37ted51SSyMsj/TLRyUjOnufQ4ACT0gTsKYmZquFrcjdZ92fpW

On 03/06/2016 04:17 PM, Gabriel Scherer wrote:

Another complementary document is

An Operational Foundation for the Tactic Language of Coq
Wojciech Jedynak, Małgorzata Biernacka, Dariusz Biernacki
2013
http://www.ii.uni.wroc.pl/~mabi/papers/PPDP13.pdf

It describes the dynamic semantics of a small fragment of Ltac, focusing in
particular on the subtle backtracking semantics of pattern-matching.

That is an interesting paper! Are the authors working on the "future work" they describe?

Are Coq developers involved in enhancing and maintaining Ltac using this paper, or something like it?

-- Jonathan

[Coq-Club] are there any formal descriptions of the tatics of Coq?, Xiaoyu Zhou, 03/06/2016
- Re: [Coq-Club] are there any formal descriptions of the tatics of Coq?, Matej Kosik, 03/06/2016
  - Re: [Coq-Club] are there any formal descriptions of the tatics of Coq?, roux cody, 03/06/2016
  - Re: [Coq-Club] are there any formal descriptions of the tatics of Coq?, Jonathan Leivent, 03/06/2016
    - Re: [Coq-Club] are there any formal descriptions of the tatics of Coq?, Gabriel Scherer, 03/06/2016
      - Re: [Coq-Club] are there any formal descriptions of the tatics of Coq?, Jonathan Leivent, 03/07/2016
    - Re: [Coq-Club] are there any formal descriptions of the tatics of Coq?, 周晓宇, 03/07/2016