Beyond Notations
(2020) : Ullrich, Sebastian de Moura, L...
DOI: https://doi.org/10.1007/978-3-030-51054-1_10
#proof_assistant #macros #coq #hygienic_transforms #my_bibtex

Structural Analysis of Narratives With the Coq Proof Assistant
(2011) : Bosser, Anne-Gwenn et al
DOI: https://doi.org/10.1007/978-3-642-22863-6_7
#narrative #structural_analysis #proof_assistant #idris #proof_theory #linear_logic #coq #my_bibtex

A Tactic Language for the System Coq
(2000) : Delahaye, David
DOI: https://doi.org/10.1007/3-540-44404-1_7
#coq #tactics #proof_assistant #ltac #my_bibtex

The Gallina Specification Language: a Case Study
(1992) : G{\'e}rard Huet
DOI: https://doi.org/10.1007/3-540-56287-7_108
#coq #gallina #predicate_logic #programming_language_design #prolog #proof_assistant #specification
#my_bibtex

A Tactic Language for the System Coq
(2000) : David Delahaye
DOI: https://doi.org/10.1007/3-540-44404-1_7
#coq #ltac #proof_assistant #tactics
#my_bibtex

proof-oriented-programming-in-fstar
(2022) : Nikhil Swamy
url: http://fstar-lang.org/tutorial/book/index.html
#dependent_types #f_star #functional_programming #proof_assistant #refinement_types
#my_bibtex