Languages Features Creators CSV Resources Challenges Add Language
GitHub icon

Coq

Coq - Programming language

< >
menu_book edit

Coq is a programming language created in 1989.

#183on PLDB 34Years Old 3.6kUsers
3Books 27Papers 5kRepos

In computer science, Coq is an interactive theorem prover. It allows the expression of mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification. Coq works within the theory of the calculus of inductive constructions, a derivative of the calculus of constructions. Read more on Wikipedia...


Example from Linguist:
Require Import FunctionNinjas.All. Require Import ListString.All. Require Import Computation. Import C.Notations. Definition error (message : LString.t) : C.t := do_call! Command.ShowError message in ret. Definition main : C.t := call! card_is_valid := Command.AskCard in if card_is_valid then call! pin := Command.AskPIN in match pin with | None => error @@ LString.s "No PIN given." | Some pin => call! pin_is_valid := Command.CheckPIN pin in if pin_is_valid then call! ask_amount := Command.AskAmount in match ask_amount with | None => error @@ LString.s "No amount given." | Some amount => call! amount_is_valid := Command.CheckAmount amount in if amount_is_valid then call! card_is_given := Command.GiveCard in if card_is_given then call! amount_is_given := Command.GiveAmount amount in if amount_is_given then ret else error @@ LString.s "Cannot give you the amount. Please contact your bank." else error @@ LString.s "Cannot give you back the card. Please contact your bank." else error @@ LString.s "Invalid amount." end else error @@ LString.s "Invalid PIN." end else error @@ LString.s "Invalid card.".

Language features

Feature Supported Token Example
Binary Literals ✓
Integers ✓
Floats ✓
Hexadecimals ✓
Octals ✓

Books about Coq from ISBNdb

title authors year publisher
Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant (The MIT Press) Chlipala, Adam 2013-12-06T00:00:01Z The MIT Press
Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant Chlipala, Adam 2022 MIT Press
Computer Arithmetic and Formal Proofs: Verifying Floating-point Algorithms with the Coq System (Computer Engineering) Boldo, Sylvie and Melquiond, Guillaume 2017 ISTE Press - Elsevier

Publications about Coq from Semantic Scholar

title authors year citations influentialCitations
Extending Coq with Imperative Features and Its Application to SAT Verification Michaël Armand and B. Grégoire and A. Spiwack and Laurent Théry 2010 76 6
Strongly Typed Term Representations in Coq Nick Benton and C. Hur and A. Kennedy and Conor McBride 2012 74 3
Canonical Structures for the Working Coq User A. Mahboubi and E. Tassi 2013 55 0
Å’uf: minimizing the Coq extraction TCB Eric Mullen and Stuart Pernsteiner and James R. Wilcox and Zachary Tatlock and D. Grossman 2018 35 1
Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq Y. Forster and G. Smolka 2017 34 3
Verification of PLC Properties Based on Formal Semantics in Coq J. Blech and Sidi Ould Biha 2011 32 1
Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq J. Bengtson and J. B. Jensen and Filip Sieczkowski and L. Birkedal 2011 31 3
Aliasing Restrictions of C11 Formalized in Coq R. Krebbers 2013 27 1
Mtac2: typed tactics for backward reasoning in Coq Jan-Oliver Kaiser and Beta Ziliani and R. Krebbers and Y. Régis-Gianas and Derek Dreyer 2018 24 1
An Introduction to Programming and Proving with Dependent Types in Coq A. Chlipala 2010 21 0
ConCert: a smart contract certification framework in Coq D. Annenkov and Bas Spitters 2019 21 2
Calculating Parallel Programs in Coq Using List Homomorphisms F. Loulergue and Wadoud Bousdira and J. Tesson 2017 16 1
Verified programming of Turing machines in Coq Y. Forster and F. Kunze and Maximilian Wuttke 2020 16 0
A Formalization of the C99 Standard in HOL, Isabelle and Coq R. Krebbers and F. Wiedijk 2011 14 0
Computational Verification of Network Programs in Coq Gordon Stewart 2013 13 1
A unification algorithm for Coq featuring universe polymorphism and overloading Beta Ziliani and Matthieu Sozeau 2015 12 0
Bringing Coq into the World of GCM Distributed Applications Nuno Gaspar and L. Henrio and E. Madelaine 2014 11 1
A Hybrid Formal Verification System in Coq for Ensuring the Reliability and Security of Ethereum-Based Service Smart Contracts Zheng Yang and Hang Lei and Weizhong Qian 2019 11 0
30 years of research and development around Coq G. Huet and Hugo Herbelin 2014 10 0
Call-by-Value Lambda Calculus as a Model of Computation in Coq Y. Forster and G. Smolka 2018 7 0
An operational foundation for the tactic language of Coq Wojciech Jedynak and Malgorzata Biernacka and Dariusz Biernacki 2013 7 0
Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs Nada Habli and A. Felty 2013 3 0
Coq à la carte: a practical approach to modular syntax with binders Y. Forster and Kathrin Stark 2020 3 0
Towards a Framework for Building Formally Verified Supercompilers in Coq D. Krustev 2012 1 0
Programming with Effects in Coq J. G. Morrisett 2008 1 0
Type- Theoretical Foundations of the Derivation System in Coq Vasyl Lenko and V. Pasichnyk and N. Kunanets and Y. Shcherbyna 2018 1 0
Interactive typed tactic programming in the Coq proof assistant Beta Ziliani 2015 1 0
occam.html · coq.html · autoit.html

View source

- Build the next great programming language · Search · Day 213 · About · Blog · Acknowledgements · Traffic · Traffic Today · GitHub · feedback@pldb.com