Language Descriptions Tools Applications

Language Descriptions - Tools and Applications

---

• http://ldta.info/

---

Grammars

• ParsingReflectiveGrammars
  • PaulStansifer? and MitchellWand?
• StepwiseEvaluationAttributeGrammars
  • ArieMiddelkoop? AtzeDijkstra? and DoaitseSwierstra?
• VLex: VisualizingLexicalAnalyzerGenerator? - Tool Demonstration
  • AlisdairJorgensen?, GiorgiosEconomopoulos? BerndFischer?
    • http://dragonbook.stanford.edu/lecture-notes/Stanford-CS143/03-Lexical-Analysis.pdf
• YieldGrammarAnalysis? Bellman's GAP compiler
  • RobertGiegerich? GeorgSauthoff?

---

Coq in computer science

• Coq
  • is an interactive theorem prover allowing the expression of mathematical assertions
  • mechanically checks proofs of these assertions
  • helps find formal proofs
  • extracts a certified program from the constructive proof of its formal specification
  • works within the theory of the calculus of inductive constructions - a derivative of the calculus of constructions.
  • is not an automated theorem prover
  • includes automatic theorem proving tactics and various decision procedures

---

CategoryComputerArchitecture