Coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. Typical applications include the formalization of programming languages semantics (e.g. the CompCert compiler certification project or Java Card EAL7 certification in industrial context), the formalization of mathematics (e.g. the full formalization of the 4 color theorem or constructive mathematics at Nijmegen) and teaching.


References in zbMATH (referenced in 1378 articles , 3 standard articles )

Showing results 1 to 20 of 1378.
Sorted by year (citations)

1 2 3 ... 67 68 69 next

  1. Boutry, Pierre; Braun, Gabriel; Narboux, Julien: Formalization of the arithmetization of Euclidean plane geometry and applications (2019)
  2. Drămnesc, Isabela; Jebelean, Tudor; Stratulat, Sorin: Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques (2019)
  3. Gauthier, Thibault; Kaliszyk, Cezary: Aligning concepts across proof assistant libraries (2019)
  4. Ahrens, Benedikt; Matthes, Ralph: Heterogeneous substitution systems revisited (2018)
  5. Angiuli, Carlo; Harper, Robert: Meaning explanations at higher dimension (2018)
  6. Ayala-Rincón, Mauricio; de Carvalho-Segundo, Washington; Fernández, Maribel; Nantes-Sobrinho, Daniele: Nominal C-unification (2018)
  7. Bertot, Yves; Rideau, Laurence; Théry, Laurent: Distant decimals of $\pi $: formal proofs of some algorithms computing them and guarantees of exact computation (2018)
  8. Biernacki, Dariusz; Polesiuk, Piotr: Logical relations for coherence of effect subtyping (2018)
  9. Cao, Qinxiang; Beringer, Lennart; Gruetter, Samuel; Dodds, Josiah; Appel, Andrew W.: VST-Floyd: a separation logic tool to verify correctness of C programs (2018)
  10. Chen, Hao; Wu, Xiongnan; Shao, Zhong; Lockerman, Joshua; Gu, Ronghui: Toward compositional verification of interruptible OS kernels and device drivers (2018)
  11. Clochard, Martin; Gondelman, Léon; Pereira, Mário: The matrix reproved (verification pearl) (2018)
  12. Czajka, Łukasz; Kaliszyk, Cezary: Hammer for Coq: automation for dependent type theory (2018)
  13. Dagand, Pierre-Évariste; Tabareau, Nicolas; Tanter, Éric: Foundations of dependent interoperability (2018)
  14. de Putter, Sander; Wijs, Anton: A formal verification technique for behavioural model-to-model transformations (2018)
  15. Doczkal, Christian; Smolka, Gert: Regular language representations in the constructive type theory of Coq (2018)
  16. Fares, Elie; Bodeveix, Jean-Paul; Filali, Mamoun: Event algebra for transition systems composition application to timed automata (2018)
  17. Farmer, William M.: Incorporating quotation and evaluation into Church’s type theory (2018)
  18. Genet, Thomas; Haudebourg, Timothée; Jensen, Thomas: Verifying higher-order functions with tree automata (2018)
  19. He, Shaobo; Lahiri, Shuvendu K.; Rakamarić, Zvonimir: Verifying relative safety, accuracy, and termination for program approximations (2018)
  20. Léchenet, Jean-Christophe; Kosmatov, Nikolai; Le Gall, Pascale: Cut branches before looking for bugs: certifiably sound verification on relaxed slices (2018)

1 2 3 ... 67 68 69 next