27 papers:
ICFP-2015-ZilianiS #algorithm #coq #morphism #polymorphism #unification- A unification algorithm for Coq featuring universe polymorphism and overloading (BZ, MS), pp. 179–191.
CC-2015-DemangePS #coq #optimisation #performance #verification- Verifying Fast and Sparse SSA-Based Optimizations in Coq (DD, DP, LS), pp. 233–252.
ESOP-2014-BenzakenCD #coq #formal method #relational- A Coq Formalization of the Relational Data Model (VB, EC, SD), pp. 189–208.
POPL-2014-HuetH #coq #development #research- 30 years of research and development around Coq (GH, HH), pp. 249–250.
- ICFP-2013-ZilianiDKNV #coq #monad #named #programming
- Mtac: a monad for typed tactic programming in Coq (BZ, DD, NRK, AN, VV), pp. 87–100.
HILT-2013-CourtieuACZRBHG #coq #formal method #runtime #semantics #towards #using- Towards the formalization of SPARK 2014 semantics with explicit run-time checks using coq (PC, MVA, TC, ZZ, R, JB, JH, JG, TJ), pp. 21–22.
PPDP-2013-JedynakBB #coq- An operational foundation for the tactic language of Coq (WJ, MB, DB), pp. 25–36.
- PPDP-2013-KennedyBJD #assembly #coq #metaprogramming #named #question
- Coq: the world’s best macro assembler? (AK, NB, JBJ, PÉD), pp. 13–24.
- PPDP-2013-KrienerKB #coq #prolog #proving #semantics
- Proofs you can believe in: proving equivalences between Prolog semantics in Coq (JK, AK, SB), pp. 37–48.
- POPL-2012-StrubSFC #coq #named #self
- Self-certification: bootstrapping certified typecheckers in F* with Coq (PYS, NS, CF, JC), pp. 571–584.
SEFM-2011-BlechB #coq #semantics #verification- Verification of PLC Properties Based on Formal Semantics in Coq (JOB, SOB), pp. 58–73.
- SEFM-2011-OnoHTNH #coq #pipes and filters #specification #using
- Using Coq in Specification and Program Extraction of Hadoop MapReduce Applications (KO, YH, YT, NN, MH), pp. 350–365.
SAS-2010-HofmannKS #coq #verification- Verifying a Local Generic Solver in Coq (MH, AK, HS), pp. 340–355.
CIAA-2010-AlmeidaMPS #automaton #coq- Partial Derivative Automata Formalized in Coq (JBA, NM, DP, SMdS), pp. 59–68.
IFL-2010-SieczkowskiBB #automation #automaton #coq #formal method #reduction #semantics- Automating Derivations of Abstract Machines from Reduction Semantics: — A Generic Formalization of Refocusing in Coq (FS, MB, DB), pp. 72–88.
SAC-2010-Pham #geometry #proving- Similar triangles and orientation in plane elementary geometry for Coq-based proofs (TMP), pp. 1268–1269.
CSL-2010-Strub #coq #modulo theories- Coq Modulo Theory (PYS), pp. 529–543.
- ESOP-2009-SchaferEM #attribute grammar #coq #formal method #verification
- Formalising and Verifying Reference Attribute Grammars in Coq (MS, TE, OdM), pp. 143–159.
- SAC-2009-MagaudNS #coq #formal method #theorem #using
- Formalizing Desargues’ theorem in Coq using ranks (NM, JN, PS), pp. 1110–1115.
- PPDP-2008-BertotK #coq #fixpoint #recursion #semantics
- Fixed point semantics and partial recursion in Coq (YB, VK), pp. 89–96.
FLOPS-2006-BartheFPR #coq #proving #reasoning #recursion- Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant (GB, JF, DP, VR), pp. 114–129.
TLCA-2003-Oury #coq #equivalence #proving- Observational Equivalence and Program Extraction in the Coq Proof Assistant (NO), pp. 271–285.
TACAS-1998-Sprenger #calculus #coq #model checking #μ-calculus- A Verified Model Checker for the Modal μ-calculus in Coq (CS), pp. 167–183.
CADE-1996-BertotB #named- CtCoq: A System Presentation (JB, YB), pp. 231–234.
- TLCA-1995-DespeyrouxFH #coq #higher-order #syntax
- Higher-Order Abstract Syntax in Coq (JD, APF, AH), pp. 124–138.
- TLCA-1995-Leclerc #coq #development #multi #order #proving #term rewriting #termination
- Termination Proof of Term Rewriting System with the Multiset Path Ordering. A Complete Development in the System Coq (FL), pp. 312–327.
- TLCA-1993-Paulin-Mohring #coq #induction
- Inductive Definitions in the system Coq — Rules and Properties (CPM), pp. 328–345.
