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