Skip to main content

Questions tagged [abstract-syntax-tree]

Use this tag with abstract syntax trees.

Filter by
Sorted by
Tagged with
1 vote
1 answer

Proof of Constant folding in Coq for IMP using Interaction Trees

Hello Stack Exchange Community, I'm currently working on my thesis which involves using Interaction Trees to define big-step operational semantics for programming languages, particularly the IMP ...
Andrea Tirelli's user avatar
1 vote
2 answers

How to parse Lean 3(?) theorem statements to JSON AST

I'd like to take a .lean file, and extract from it all the theorem statements into a fully-elaborated unambiguous textual format that is morally isomorphic to the ...
Michael Norrish's user avatar
0 votes
1 answer

Induction error on mutually defined types in Coq

I want to define two types that depend on each other ...
matteo_c's user avatar
  • 131
0 votes
1 answer

How do you implement what's in the Pierce Book precisely? And why / why not have evaluation just mutate ParseTree's of a PEG parser generator library?

Here is a link to the "Pierce Book" or Benjamin Pierce's draft transcript of (the first part of) "Types and Programming Languages". On PDF page 28 you'll see an OCaml ...
HighAsAKiteOnMath's user avatar
1 vote
1 answer

How does Lean4 (or a typical PA) represent lambda functions or in other words arbitrary expressions?

Question: Say I wanted my language to support various operator symbols, the semantics of which are defined by the user or by axioms. I'm wondering whether Lean4 (or a typical well-known PA) just ...
HighAsAKiteOnMath's user avatar
6 votes
0 answers

How does one systematically traverse OCaml representations of Coq ASTs terms?

I want to be able to (tree) traverse Coq terms (e.g. in OCaml or using their s-expression representation in any language). My main challenge is to figure out how to do this systematically because I ...
Charlie Parker's user avatar
8 votes
1 answer

How to deal with the proliferation of encodings of ASTs?

When working with type theory and ASTs one often ends up with a large amount of different encodings. It's very similar to the same problem in compiler design but more annoying because it's dependently ...
Ms. Molly Stewart-Gallus's user avatar