coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] coq abstract syntax tree

From: Adam Chlipala <adamc AT hcoop.net>
To: Damien Andrew Tamburri <maelstrom_dat AT hotmail.com>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] coq abstract syntax tree
Date: Sun, 06 Sep 2009 19:54:29 -0400
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Damien Andrew Tamburri wrote:

    I am trying to formalize a simplified version of an abstract
    syntax tree data structure in COQ. is anyone aware if there's any
    module for COQ defining the representation of an actual program in
    a programming language? is there any representation of ASTs within
    Coq already developed that I can take a look at? does anyone
    pursue such a work already?

"Abstract syntax tree" is a pretty general concept. You might be interested in the numerous examples of program syntax manipulation that appear in my draft book:
http://adam.chlipala.net/cpdt/

Re: [Coq-Club] coq abstract syntax tree, Adam Chlipala