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