Skip to content
scrambled
Programming Language Theory Concept

Proof

JourneyProgramming Language Theory Statusreviewing Tags
  • formal system
  • language feature design
  • logic
  • programming paradigm
  • proof reason technique

Tools: Rocq (formerly Coq)

  • (Logic, Proof/Reason technique) A logical argument establishing the truth of a proposition.

  • (Language feature/design, Programming paradigm, Formal system, Proof/Reason technique) In Rocq, a term of a propositional type constructed interactively via tactics or directly as a term. This draws from the Curry-Howard correspondence.