Tag #coq
49 papers:
POPL-2020-SozeauBFTW #exclamation #type checking #verification- Coq Coq correct! verification of type checking and erasure for Coq, in Coq (MS, SB, YF0, NT, TW), p. 28.
- POPL-2020-XiaZHHMPZ #interactive #recursion #representation #source code
- Interaction trees: representing recursive and impure programs in Coq (LyX, YZ, PH, CKH, GM, BCP, SZ), p. 32.
FSCD-2019-Larchey-Wendling #problem- Hilbert's Tenth Problem in Coq (DLW, YF0), p. 20.
Haskell-2019-ChristiansenDB #haskell #source code #verification- Verifying effectful Haskell programs in Coq (JC, SD, NB), pp. 125–138.
- ICFP-2019-SozeauM #equation #functional #programming #proving
- Equations reloaded: high-level dependently-typed functional programming and proving in Coq (MS, CM), p. 29.
ASE-2019-CelikPPAG #analysis #mutation testing- Mutation Analysis for Coq (AÇ, KP, MP, EJGA, MG), pp. 539–551.
FM-2018-LetanRCH #composition #source code #verification- Modular Verification of Programs with Effects and Effect Handlers in Coq (TL, YRG, PC, GH), pp. 338–354.
- FSCD-2018-TimanyS #cumulative #induction
- Cumulative Inductive Types In Coq (AT, MS), p. 16.
- ICFP-2018-KaiserZKRD #named #reasoning
- Mtac2: typed tactics for backward reasoning in Coq (JOK, BZ, RK, YRG, DD), p. 31.
ICMT-2018-TisiC #domain-specific language #model transformation #named- CoqTL: An Internal DSL for Model Transformation in Coq (MT, ZC), pp. 142–156.
ESOP-2018-RahliVVV #fault tolerance #named #protocol- Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq (VR, IV, MV, PJEV), pp. 619–650.
- FSCD-2017-KaiserPS #case study #system f
- Relating System F and Lambda2: A Case Study in Coq, Abella and Beluga (JK, BP, GS), p. 19.
- IFM-2017-FerreiraJMB #authentication #case study #linux #quality #using
- Certified Password Quality - A Case Study Using Coq and Linux Pluggable Authentication Modules (JFF, SAJ, AM, PJB), pp. 407–421.
- Haskell-2017-VazouLP #haskell #proving #string #verification
- A tale of two provers: verifying monoidal string matching in liquid Haskell and Coq (NV, LL, JP), pp. 63–74.
- Haskell-2017-WiegleyD #haskell #performance #using
- Using Coq to write fast and correct Haskell (JW, BD), pp. 52–62.
- ICFP-2017-AuerbachHMSS #case study #compilation #experience #prototype #query #using
- Prototyping a query compiler using Coq (experience report) (JSA, MH, LM, AS, JS), p. 15.
CAV-2017-Carbonneaux0RS #analysis #automation #proving- Automated Resource Analysis with Coq Proof Objects (QC, JH0, TWR, ZS), pp. 64–85.
- CAV-2017-EkiciMTKKRB #named #plugin #smt
- SMTCoq: A Plug-In for Integrating SMT Solvers into Coq (BE, AM, CT, CK, GK, AR, CWB), pp. 126–133.
- FM-2016-SenjakH #implementation
- An Implementation of Deflate in Coq (CSS, MH0), pp. 612–627.
- FSCD-2016-Timany0 #category theory
- Category Theory in Coq 8.5 (AT, BJ0), p. 18.
SEFM-2016-ZhangQ #framework #implementation #object-oriented #verification- Coq Implementation of OO Verification Framework VeriJ (KZ, ZQ), pp. 270–276.
PPDP-2016-Morrisett #challenge #compilation- Challenges in compiling Coq (GM), p. 9.
ICFP-2015-ZilianiS #algorithm #morphism #polymorphism #unification- A unification algorithm for Coq featuring universe polymorphism and overloading (BZ, MS), pp. 179–191.
CC-2015-DemangePS #optimisation #performance #verification- Verifying Fast and Sparse SSA-Based Optimizations in Coq (DD, DP, LS), pp. 233–252.
- POPL-2014-HuetH #development #research
- 30 years of research and development around Coq (GH, HH), pp. 249–250.
- ESOP-2014-BenzakenCD #formal method #relational
- A Coq Formalization of the Relational Data Model (VB, EC, SD), pp. 189–208.
- ICFP-2013-ZilianiDKNV #monad #named #programming
- Mtac: a monad for typed tactic programming in Coq (BZ, DD, NRK, AN, VV), pp. 87–100.
HILT-2013-CourtieuACZRBHG #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
- An operational foundation for the tactic language of Coq (WJ, MB, DB), pp. 25–36.
- PPDP-2013-KennedyBJD #assembly #metaprogramming #named #question
- Coq: the world’s best macro assembler? (AK, NB, JBJ, PÉD), pp. 13–24.
- PPDP-2013-KrienerKB #prolog #proving #semantics
- Proofs you can believe in: proving equivalences between Prolog semantics in Coq (JK, AK, SB), pp. 37–48.
- Haskell-2012-Swierstra #case study #experience #programming #proving
- xmonad in Coq (experience report): programming a window manager in a proof assistant (WS), pp. 131–136.
- POPL-2012-StrubSFC #named #self
- Self-certification: bootstrapping certified typecheckers in F* with Coq (PYS, NS, CF, JC), pp. 571–584.
- SEFM-2011-BlechB #semantics #verification
- Verification of PLC Properties Based on Formal Semantics in Coq (JOB, SOB), pp. 58–73.
- SEFM-2011-OnoHTNH #pipes and filters #specification #using
- Using Coq in Specification and Program Extraction of Hadoop MapReduce Applications (KO, YH, YT, NN, MH), pp. 350–365.
CIAA-2010-AlmeidaMPS #automaton- Partial Derivative Automata Formalized in Coq (JBA, NM, DP, SMdS), pp. 59–68.
- Haskell-2010-PirogB
- A systematic derivation of the STG machine verified in Coq (MP, DB), pp. 25–36.
IFL-2010-SieczkowskiBB #automation #automaton #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.
SAS-2010-HofmannKS #verification- Verifying a Local Generic Solver in Coq (MH, AK, HS), pp. 340–355.
CSL-2010-Strub #modulo theories- Coq Modulo Theory (PYS), pp. 529–543.
SAC-2009-MagaudNS #formal method #theorem #using- Formalizing Desargues’ theorem in Coq using ranks (NM, JN, PS), pp. 1110–1115.
- ESOP-2009-SchaferEM #attribute grammar #formal method #verification
- Formalising and Verifying Reference Attribute Grammars in Coq (MS, TE, OdM), pp. 143–159.
- PPDP-2008-BertotK #fixpoint #recursion #semantics
- Fixed point semantics and partial recursion in Coq (YB, VK), pp. 89–96.
FLOPS-2006-BartheFPR #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 #equivalence #proving- Observational Equivalence and Program Extraction in the Coq Proof Assistant (NO), pp. 271–285.
TACAS-1998-Sprenger #calculus #model checking #μ-calculus- A Verified Model Checker for the Modal μ-calculus in Coq (CS), pp. 167–183.
- TLCA-1995-DespeyrouxFH #higher-order #syntax
- Higher-Order Abstract Syntax in Coq (JD, APF, AH), pp. 124–138.
- TLCA-1995-Leclerc #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 #induction
- Inductive Definitions in the system Coq — Rules and Properties (CPM), pp. 328–345.
