Search results for "coq"

Hits ?▲	Authors	Title	Venue	Year	Link
16	Grygoriy Zholtkevych	Event Universes: Specification and Analysis Using Coq Proof Assistant.	ICTERI Workshops	2019	DBLP BibTeX RDF
16	Pascal Fradet, Xiaojie Guo 0003, Jean-François Monin, Sophie Quinton	CertiCAN: A Tool for the Coq Certification of CAN Analysis Results.	RTAS	2019	DBLP DOI BibTeX RDF
16	Guillaume Bertholon, Érik Martin-Dorel, Pierre Roux	Primitive Floats in Coq.	ITP	2019	DBLP DOI BibTeX RDF
16	Talia Ringer, Nathaniel Yazdani, John Leo, Dan Grossman	Ornaments for Proof Reuse in Coq.	ITP	2019	DBLP DOI BibTeX RDF
16	Florian Steinberg 0001, Laurent Théry, Holger Thies	Quantitative Continuity and Computable Analysis in Coq.	ITP	2019	DBLP DOI BibTeX RDF
16	Ran Chen, Cyril Cohen, Jean-Jacques Lévy, Stephan Merz, Laurent Théry	Formal Proofs of Tarjan's Strongly Connected Components Algorithm in Why3, Coq and Isabelle.	ITP	2019	DBLP DOI BibTeX RDF
16	Lukasz Czajka 0001	First-Order Guarded Coinduction in Coq.	ITP	2019	DBLP DOI BibTeX RDF
16	Yannick Forster 0002, Fabian Kunze	A Certifying Extraction with Time Bounds from Coq to Call-By-Value Lambda Calculus.	ITP	2019	DBLP DOI BibTeX RDF
16	Yannick Forster 0002, Steven Schäfer, Simon Spies, Kathrin Stark	Call-by-push-value in coq: operational, equational, and denotational theory.	CPP	2019	DBLP DOI BibTeX RDF
16	Yannick Forster 0002, Dominik Kirst, Gert Smolka	On synthetic undecidability in coq, with an application to the entscheidungsproblem.	CPP	2019	DBLP DOI BibTeX RDF
16	Véronique Benzaken, Evelyne Contejean	A Coq mechanised formal semantics for realistic SQL queries: formally reconciling SQL and bag relational algebra.	CPP	2019	DBLP DOI BibTeX RDF
16	Dominique Larchey-Wendling, Yannick Forster 0002	Hilbert's Tenth Problem in Coq.	FSCD	2019	DBLP DOI BibTeX RDF
16	Ahmet Çelik, Karl Palmskog, Marinela Parovic, Emilio Jesús Gallego Arias, Milos Gligoric 0001	Mutation Analysis for Coq.	ASE	2019	DBLP DOI BibTeX RDF
16	Jan Christiansen, Sandra Dylus, Niels Bunkenburg	Verifying effectful Haskell programs in Coq.	Haskell@ICFP	2019	DBLP DOI BibTeX RDF
16	Xiyue Zhang, Yi Li 0010, Weijiang Hong, Meng Sun 0002	Using Recurrent Neural Network to Predict Tactics for Proving Component Connector Properties in Coq.	TASE	2019	DBLP DOI BibTeX RDF
16	Claudio Sacerdoti Coen	A Plugin to Export Coq Libraries to XML.	CICM	2019	DBLP DOI BibTeX RDF
16	Dennis Müller 0001, Florian Rabe 0001, Claudio Sacerdoti Coen	The Coq Library as a Theory Graph.	CICM	2019	DBLP DOI BibTeX RDF
16	Joachim Breitner, Antal Spector-Zabusky, Yao Li 0004, Christine Rizkallah, John Wiegley, Stephanie Weirich	Ready, set, verify! applying hs-to-coq to real-world Haskell code (experience report).	Proc. ACM Program. Lang.	2018	DBLP DOI BibTeX RDF
16	Jan-Oliver Kaiser, Beta Ziliani, Robbert Krebbers, Yann Régis-Gianas, Derek Dreyer	Mtac2: typed tactics for backward reasoning in Coq.	Proc. ACM Program. Lang.	2018	DBLP DOI BibTeX RDF
16	Akira Tanaka, Reynald Affeldt, Jacques Garrigue	Safe Low-level Code Generation in Coq Using Monomorphization and Monadification.	J. Inf. Process.	2018	DBLP DOI BibTeX RDF
16	Alexander John Faithfull, Jesper Bengtson, Enrico Tassi, Carst Tankink	Coqoon - An IDE for interactive proof development in Coq.	Int. J. Softw. Tools Technol. Transf.	2018	DBLP DOI BibTeX RDF
16	Joachim Breitner, Antal Spector-Zabusky, Yao Li 0004, Christine Rizkallah, John Wiegley, Stephanie Weirich	Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code.	CoRR	2018	DBLP BibTeX RDF
16	Ran Chen, Cyril Cohen, Jean-Jacques Lévy, Stephan Merz, Laurent Théry	Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle.	CoRR	2018	DBLP BibTeX RDF
16	Yves Bertot	Formal Verification of a Geometry Algorithm: A Quest for Abstract Views and Symmetry in Coq Proofs.	CoRR	2018	DBLP BibTeX RDF
16	Moez A. AbdelGawad	Finitary-based Domain Theory in Coq: An Early Report.	CoRR	2018	DBLP BibTeX RDF
16	Zheng Yang 0007, Hang Lei	FEther: An Extensible Definitional Interpreter for Smart-contract Verifications in Coq.	CoRR	2018	DBLP BibTeX RDF
16	Lukasz Czajka 0001, Burak Ekici, Cezary Kaliszyk	Concrete Semantics with Coq and CoqHammer.	CoRR	2018	DBLP BibTeX RDF
16	Artem Yushkovskiy, Stavros Tripakis	Comparison of Two Theorem Provers: Isabelle/HOL and Coq.	CoRR	2018	DBLP BibTeX RDF
16	Zheng Yang 0007, Hang Lei	A general formal memory framework in Coq for verifying the properties of programs based on higher-order logic theorem proving with increased automation, consistency, and reusability.	CoRR	2018	DBLP BibTeX RDF
16	Lukasz Czajka 0001, Cezary Kaliszyk	Hammer for Coq: Automation for Dependent Type Theory.	J. Autom. Reason.	2018	DBLP DOI BibTeX RDF
16	Christian Doczkal, Gert Smolka	Regular Language Representations in the Constructive Type Theory of Coq.	J. Autom. Reason.	2018	DBLP DOI BibTeX RDF
16	João Alpuim, Wouter Swierstra	Embedding the refinement calculus in Coq.	Sci. Comput. Program.	2018	DBLP DOI BibTeX RDF
16	Jay A. McCarthy, Burke Fetscher, Max S. New, Daniel Feltey, Robert Bruce Findler	A Coq library for internal verification of running-times.	Sci. Comput. Program.	2018	DBLP DOI BibTeX RDF
16	Xiyue Zhang, Meng Sun 0002	Towards Formal Modeling and Verification of Probabilistic Connectors in Coq (S).	SEKE	2018	DBLP DOI BibTeX RDF
16	Yves Bertot	Formal Verification of a Geometry Algorithm: A Quest for Abstract Views and Symmetry in Coq Proofs.	ICTAC	2018	DBLP DOI BibTeX RDF
16	Massimo Tisi, Zheng Cheng	CoqTL: An Internal DSL for Model Transformation in Coq.	ICMT	2018	DBLP DOI BibTeX RDF
16	Thomas Letan, Yann Régis-Gianas, Pierre Chifflier, Guillaume Hiet	Modular Verification of Programs with Effects and Effect Handlers in Coq.	FM	2018	DBLP DOI BibTeX RDF
16	Hideyuki Kawabata, Yuta Tanaka, Mai Kimura, Tetsuo Hironaka	Traf: A Graphical Proof Tree Viewer Cooperating with Coq Through Proof General.	APLAS	2018	DBLP DOI BibTeX RDF
16	Youssef El Bakouny, Dani Mezher	Scallina: Translating Verified Programs from Coq to Scala.	APLAS	2018	DBLP DOI BibTeX RDF
16	Vincent Rahli, Ivana Vukotic, Marcus Völp, Paulo Jorge Esteves Veríssimo	Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq.	ESOP	2018	DBLP DOI BibTeX RDF
16	Jérémy Buisson, Seidali Rehab	Effective Bridging Between Ecore and Coq: Case of a Type-Checker with Proof-Carrying Code.	MISC	2018	DBLP DOI BibTeX RDF
16	Catherine Dubois, Sulyvan Weppe	Towards Coq Formalisation of {log} Set Constraints Resolution.	SETS@ABZ	2018	DBLP BibTeX RDF
16	Pascal Fradet, Maxime Lesourd, Jean-François Monin, Sophie Quinton	A Generic Coq Proof of Typical Worst-Case Analysis.	RTSS	2018	DBLP DOI BibTeX RDF
16	Youssef El Bakouny, Dani Mezher	The Scallina Grammar - Towards a Scala Extraction for Coq.	SBMF	2018	DBLP DOI BibTeX RDF
16	Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, Nicolas Tabareau	Towards Certified Meta-Programming with Typed Template-Coq.	ITP	2018	DBLP DOI BibTeX RDF
16	Sylvain Boulmé, Alexandre Maréchal	A Coq Tactic for Equality Learning in Linear Arithmetic.	ITP	2018	DBLP DOI BibTeX RDF
16	Yannick Forster 0002, Edith Heiter, Gert Smolka	Verification of PCP-Related Computational Reductions in Coq.	ITP	2018	DBLP DOI BibTeX RDF
16	Étienne Miquey	Formalizing Implicative Algebras in Coq.	ITP	2018	DBLP DOI BibTeX RDF
16	Véronique Benzaken, Evelyne Contejean, Chantal Keller, Eunice Martins	A Coq Formalisation of SQL's Execution Engines.	ITP	2018	DBLP DOI BibTeX RDF
16	Pawel Wieczorek, Dariusz Biernacki	A Coq formalization of normalization by evaluation for Martin-Löf type theory.	CPP	2018	DBLP DOI BibTeX RDF
16	Damien Rouhling	A formal proof in Coq of a control function for the inverted pendulum.	CPP	2018	DBLP DOI BibTeX RDF
16	Eric Mullen, Stuart Pernsteiner, James R. Wilcox, Zachary Tatlock, Dan Grossman	Œuf: minimizing the Coq extraction TCB.	CPP	2018	DBLP DOI BibTeX RDF
16	Sergueï Lenglet, Alan Schmitt	HOπ in Coq.	CPP	2018	DBLP DOI BibTeX RDF
16	Christian Doczkal, Joachim Bard	Completeness and decidability of converse PDL in the constructive type theory of Coq.	CPP	2018	DBLP DOI BibTeX RDF
16	Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, Stephanie Weirich	Total Haskell is reasonable Coq.	CPP	2018	DBLP DOI BibTeX RDF
16	Amin Timany, Matthieu Sozeau	Cumulative Inductive Types In Coq.	FSCD	2018	DBLP DOI BibTeX RDF
16	Salwa Souaf, Frédéric Loulergue	Strong Security Guarantees: From Alloy to Coq (Research Poster).	HPCS	2018	DBLP DOI BibTeX RDF
16	Heiko Becker, Nikita Zyuzin, Raphaël Monat, Eva Darulova, Magnus O. Myreen, Anthony C. J. Fox	A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4.	FMCAD	2018	DBLP DOI BibTeX RDF
16	Ahmet Çelik, Karl Palmskog, Milos Gligoric 0001	A regression proof selection tool for coq.	ICSE (Companion Volume)	2018	DBLP DOI BibTeX RDF
16	David Braun, Nicolas Magaud, Pascal Schreck	Formalizing Some "Small" Finite Models of Projective Geometry in Coq.	AISC	2018	DBLP DOI BibTeX RDF
16	Diane Gallois-Wong, Sylvie Boldo, Thibault Hilaire	A Coq Formalization of Digital Filters.	CICM	2018	DBLP DOI BibTeX RDF
16	Burak Ekici	Towards Mac Lane's Comparison Theorem for the (co)Kleisli Construction in Coq.	CICM Workshops	2018	DBLP BibTeX RDF
16	Lukasz Czajka 0001, Burak Ekici, Cezary Kaliszyk	Concrete Semantics with Coq and CoqHammer.	CICM	2018	DBLP DOI BibTeX RDF
16	Joshua S. Auerbach, Martin Hirzel, Louis Mandel, Avraham Shinnar, Jérôme Siméon	Prototyping a query compiler using Coq (experience report).	Proc. ACM Program. Lang.	2017	DBLP DOI BibTeX RDF
16	Tiago Cogumbreiro, Jun Shirako, Vivek Sarkar	Formalization of Habanero phasers using Coq.	J. Log. Algebraic Methods Program.	2017	DBLP DOI BibTeX RDF
16	Bruno Xavier, Carlos Olarte, Giselle Reis, Vivek Nigam	Mechanizing Focused Linear Logic in Coq.	LSFA	2017	DBLP DOI BibTeX RDF
16	Polina Vinogradova, Amy P. Felty, Philip J. Scott	Formalizing Abstract Computability: Turing Categories in Coq.	LSFA	2017	DBLP DOI BibTeX RDF
16	Frédéric Loulergue, Wadoud Bousdira, Julien Tesson	Calculating Parallel Programs in Coq Using List Homomorphisms.	Int. J. Parallel Program.	2017	DBLP DOI BibTeX RDF
16	Alexander Bagnall, Samuel Merten, Gordon Stewart 0001	A Library for Algorithmic Game Theory in Ssreflect/Coq.	J. Formaliz. Reason.	2017	DBLP DOI BibTeX RDF
16	Sebastian Böhne, Christoph Kreitz	Learning how to Prove: From the Coq Proof Assistant to Textbook Style.	ThEdu@CADE	2017	DBLP DOI BibTeX RDF
16	Youssef El Bakouny, Tristan Crolard, Dani Mezher	A Coq-based synthesis of Scala programs which are correct-by-construction.	CoRR	2017	DBLP BibTeX RDF
16	Yannick Forster 0002, Edith Heiter, Gert Smolka	Verification of PCP-Related Computational Reductions in Coq.	CoRR	2017	DBLP BibTeX RDF
16	Andrew Bedford	Coqatoo: Generating Natural Language Versions of Coq Proofs.	CoRR	2017	DBLP BibTeX RDF
16	Robert Rand 0001, Jennifer Paykin, Steve Zdancewic	QWIRE Practice: Formal Verification of Quantum Circuits in Coq.	QPL	2017	DBLP DOI BibTeX RDF
16	Stéphane Le Roux 0001, Érik Martin-Dorel, Jan-Georg Smaus	An Existence Theorem of Nash Equilibrium in Coq and Isabelle.	GandALF	2017	DBLP DOI BibTeX RDF
16	Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, Stephanie Weirich	Total Haskell is Reasonable Coq.	CoRR	2017	DBLP BibTeX RDF
16	Sylvie Boldo, Guillaume Melquiond	Computer Arithmetic and Formal Proofs - Verifying Floating-point Algorithms with the Coq System.		2017	RDF
16	Hernan M. Palombo, Hao Zheng 0001, Jay Ligatti	POSTER: Towards Precise and Automated Verification of Security Protocols in Coq.	CCS	2017	DBLP DOI BibTeX RDF
16	Kenneth Roe, Scott F. Smith 0001	Using the coq theorem prover to verify complex data structure invariants.	MEMOCODE	2017	DBLP DOI BibTeX RDF
16	Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds 0001, Clark W. Barrett	SMTCoq: A Plug-In for Integrating SMT Solvers into Coq.	CAV (2)	2017	DBLP DOI BibTeX RDF
16	Quentin Carbonneaux, Jan Hoffmann 0002, Thomas W. Reps, Zhong Shao	Automated Resource Analysis with Coq Proof Objects.	CAV (2)	2017	DBLP DOI BibTeX RDF
16	Youssef El Bakouny, Tristan Crolard, Dani Mezher	A Coq-based synthesis of Scala programs which are correct-by-construction.	FTfJP@ECOOP	2017	DBLP DOI BibTeX RDF
16	Jean-Philippe Bernardy, Stergios Chatzikyriakidis	A Type-Theoretical system for the FraCaS test suite: Grammatical Framework meets Coq.	IWCS(1)	2017	DBLP BibTeX RDF
16	Xiaojie Guo 0003, Sophie Quinton, Pascal Fradet, Jean-François Monin	Work-in-Progress: Toward a Coq-Certified Tool for the Schedulability Analysis of Tasks with Offsets.	RTSS	2017	DBLP DOI BibTeX RDF
16	João F. Ferreira 0001, Saul A. Johnson, Alexandra Mendes, Phillip J. Brooke	Certified Password Quality - A Case Study Using Coq and Linux Pluggable Authentication Modules.	IFM	2017	DBLP DOI BibTeX RDF
16	Yannick Forster 0002, Gert Smolka	Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq.	ITP	2017	DBLP DOI BibTeX RDF
16	Dominique Larchey-Wendling	Typing Total Recursive Functions in Coq.	ITP	2017	DBLP DOI BibTeX RDF
16	Cyril Cohen, Damien Rouhling	A Formal Proof in Coq of LaSalle's Invariance Principle.	ITP	2017	DBLP DOI BibTeX RDF
16	Jiawei Wang, Ming Fu, Lei Qiao, Xinyu Feng 0001	Formalizing SPARCv8 Instruction Set Architecture in Coq.	SETTA	2017	DBLP DOI BibTeX RDF
16	Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, Bas Spitters	The HoTT library: a formalization of homotopy type theory in Coq.	CPP	2017	DBLP DOI BibTeX RDF
16	Jonas Kaiser, Tobias Tebbi, Gert Smolka	Equivalence of system f and ź2 in Coq based on context morphism lemmas.	CPP	2017	DBLP DOI BibTeX RDF
16	Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero	A Coq formal proof of the LaxMilgram theorem.	CPP	2017	DBLP DOI BibTeX RDF
16	Jonas Kaiser, Brigitte Pientka, Gert Smolka	Relating System F and Lambda2: A Case Study in Coq, Abella and Beluga.	FSCD	2017	DBLP DOI BibTeX RDF
16	Jolan Philippe, Wadoud Bousdira, Frédéric Loulergue	Formalization of a Big Graph API in Coq.	HPCS	2017	DBLP DOI BibTeX RDF
16	Niki Vazou, Leonidas Lampropoulos, Jeff Polakow	A tale of two provers: verifying monoidal string matching in liquid Haskell and Coq.	Haskell	2017	DBLP DOI BibTeX RDF
16	John Wiegley, Benjamin Delaware	Using Coq to write fast and correct Haskell.	Haskell	2017	DBLP DOI BibTeX RDF
16	Boris Shingarov	Programming a Smalltalk VM in Coq.	IWST	2017	DBLP DOI BibTeX RDF
16	Zhenwei Ma, Gang Chen	Formal Derivation and Verification of Coordinate Transformations in Theorem Prover Coq.	DSA	2017	DBLP DOI BibTeX RDF
16	Yifei Wang, Gang Chen	Formalization of Laplace Transform in Coq.	DSA	2017	DBLP DOI BibTeX RDF
16	Weijiang Hong, M. Saqib Nawaz, Xiyue Zhang, Yi Li 0010, Meng Sun 0002	Using Coq for Formal Modeling and Verification of Timed Connectors.	SEFM Workshops	2017	DBLP DOI BibTeX RDF