• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Pfcs
        • Proof-support
        • Semantics
        • Lifting
        • R1cs-subset
        • Indexed-names
        • Well-formedness
        • Abstract-syntax
          • Syntax-abstraction
          • Abstract-syntax-trees
          • Abstract-syntax-operations
          • Convenience-constructors
        • Concrete-syntax
        • R1cs-bridge
        • Parser-interface
      • Wp-gen
      • Dimacs-reader
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
      • Riscv
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Taspi
      • Bitcoin
      • Des
      • Ethereum
      • X86isa
      • Sha-2
      • Yul
      • Zcash
      • Proof-checker-itp13
      • Regex
      • ACL2-programming-language
      • Json
      • Jfkr
      • Equational
      • Cryptography
      • Poseidon
      • Where-do-i-place-my-book
      • Axe
      • Aleo
      • Bigmems
      • Builtins
      • Execloader
      • Solidity
      • Paco
      • Concurrent-programs
      • Bls12-377-curves
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Pfcs

Abstract-syntax

Abstract syntax of PFCSes.

We define an abstract syntax straightforwardly derived from the concrete syntax.

Besides the abstract syntax trees (ASTs), we define some operations on ASTs, and some constructors to conveniently build ASTs. We also define a notion of indexed names, useful for building ``parameterized'' PFCSes.

We also formalize the mapping from the concrete syntax trees (CSTs) defined by the grammar to the corresponding ASTs.

Subtopics

Syntax-abstraction
Mapping from concrete to abstract syntax, for PFCS.
Abstract-syntax-trees
Abstract syntax trees of PFCSes.
Abstract-syntax-operations
Operations on the abstract syntax of PFCSes.
Convenience-constructors
Utilities to convniently construct PFCS abstract syntax.