Search results for "coq"

Hits ?▲	Authors	Title	Venue	Year	Link
16	Daniel Ricketts 0001	Verification of Sampled-Data Systems using Coq.		2017	RDF
16	Izumi Asakura, Hidehiko Masuhara, Tomoyuki Aotani	Proof of Soundness of Concurrent Separation Logic for GPGPU in Coq.	J. Inf. Process.	2016	DBLP DOI BibTeX RDF
16	José Grimm	Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two, From Natural Numbers to Real Numbers.	J. Formaliz. Reason.	2016	DBLP DOI BibTeX RDF
16	Christoph-Simon Senjak, Martin Hofmann 0001	An implementation of Deflate in Coq.	CoRR	2016	DBLP BibTeX RDF
16	Jacques D. Fleuriot, Steven Obua, Phil Scott	Social Network Processes in the Isabelle and Coq Theorem Proving Communities.	CoRR	2016	DBLP BibTeX RDF
16	Guillaume Cano, Cyril Cohen, Maxime Dénès, Anders Mörtberg, Vincent Siles	Formalized linear algebra over Elementary Divisor Rings in Coq.	Log. Methods Comput. Sci.	2016	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.	CoRR	2016	DBLP BibTeX RDF
16	François Clément, Vincent Martin	The Lax-Milgram Theorem. A detailed proof to be formalized in Coq.	CoRR	2016	DBLP BibTeX RDF
16	Fabian Kunze	Towards the Integration of an Intuitionistic First-Order Prover into Coq.	HaTT@IJCAR	2016	DBLP DOI BibTeX RDF
16	Lukasz Czajka 0001, Cezary Kaliszyk	Goal Translation for a Hammer for Coq (Extended Abstract).	HaTT@IJCAR	2016	DBLP DOI BibTeX RDF
16	Allyx Fontaine, Akka Zemmari	RDA: A Coq Library to Reason about Randomised Distributed Algorithms in the Message Passing Model.	Sci. Ann. Comput. Sci.	2016	DBLP BibTeX RDF
16	Érik Martin-Dorel, Guillaume Melquiond	Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq.	J. Autom. Reason.	2016	DBLP DOI BibTeX RDF
16	Théo Zimmermann	Design and development of a tool based on Coq to write and format mathematical proofs.	FM4M/MathUI/ThEdu/DP/WIP@CIKM	2016	DBLP BibTeX RDF
16	Allyx Fontaine, Akka Zemmari	Certified Impossibility Results and Analyses in Coq of Some Randomised Distributed Algorithms.	ICTAC	2016	DBLP DOI BibTeX RDF
16	Christoph-Simon Senjak, Martin Hofmann 0001	An Implementation of Deflate in Coq.	FM	2016	DBLP DOI BibTeX RDF
16	Robbert Krebbers, Louis Parlant, Alexandra Silva 0001	Moessner's Theorem: An Exercise in Coinductive Reasoning in Coq.	Theory and Practice of Formal Methods	2016	DBLP DOI BibTeX RDF
16	Lin Qian, Zhenhua Duan, Nan Zhang 0001, Cong Tian	A Proof System for MSVL Programs in Coq.	SOFL+MSVL	2016	DBLP DOI BibTeX RDF
16	Jacek Chrzaszcz, Aleksy Schubert, Jakub Zakrzewski 0001	Coq Support in HAHA.	TYPES	2016	DBLP DOI BibTeX RDF
16	Philip Johnson-Freyd, Geoffrey C. Hulette, Zena M. Ariola	Verification by Way of Refinement: A Case Study in the Use of Coq and TLA in the Design of a Safety Critical System.	FMICS-AVoCS	2016	DBLP DOI BibTeX RDF
16	Wouter Swierstra, João Alpuim	From Proposition to Program - Embedding the Refinement Calculus in Coq.	FLOPS	2016	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.	FLOPS	2016	DBLP DOI BibTeX RDF
16	Arthur Blot, Pierre-Évariste Dagand, Julia Lawall	From Sets to Bits in Coq.	FLOPS	2016	DBLP DOI BibTeX RDF
16	Alexander John Faithfull, Jesper Bengtson, Enrico Tassi, Carst Tankink	Coqoon - An IDE for Interactive Proof Development in Coq.	TACAS	2016	DBLP DOI BibTeX RDF
16	Greg Morrisett	Challenges in compiling Coq.	PPDP	2016	DBLP DOI BibTeX RDF
16	Xiyue Zhang, Weijiang Hong, Yi Li 0010, Meng Sun 0002	Reasoning About Connectors in Coq.	FACS	2016	DBLP DOI BibTeX RDF
16	Christian Doczkal, Gert Smolka	Two-Way Automata in Coq.	ITP	2016	DBLP DOI BibTeX RDF
16	Paul Brunet, Damien Pous, Insa Stucke	Cardinalities of Finite Relations in Coq.	ITP	2016	DBLP DOI BibTeX RDF
16	Paolo Torrini	Modular Dependent Induction in Coq, Mendler-Style.	ITP	2016	DBLP DOI BibTeX RDF
16	Hiroaki Date, Noriaki Yoshiura	Computational Verification of Network Programs for Several OpenFlow Switches in Coq.	ICCSA (2)	2016	DBLP DOI BibTeX RDF
16	Sebastian Böhne, Maria Knobelsdorf, Christoph Kreitz	Mathematisches Argumentieren und Beweisen mit dem Theorembeweiser Coq.	HDI	2016	DBLP BibTeX RDF
16	Tahina Ramananandro, Paul Mountcastle, Benoît Meister, Richard Lethin	A unified Coq framework for verifying C programs with floating-point computations.	CPP	2016	DBLP DOI BibTeX RDF
16	Amin Timany, Bart Jacobs 0002	Category Theory in Coq 8.5.	FSCD	2016	DBLP DOI BibTeX RDF
16	Sorin Stratulat	Structural vs. Cyclic Induction: A Report on Some Experiments with Coq.	SYNASC	2016	DBLP DOI BibTeX RDF
16	Ke Zhang, Zongyan Qiu	Coq Implementation of OO Verification Framework VeriJ.	SEFM	2016	DBLP DOI BibTeX RDF
16	Nelma Moreira, David Pereira, Simão Melo de Sousa	Deciding Kleene algebra terms equivalence in Coq.	J. Log. Algebraic Methods Program.	2015	DBLP DOI BibTeX RDF
16	Nicolas Magaud, Agathe Chollet, Laurent Fuchs	Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective.	Ann. Math. Artif. Intell.	2015	DBLP DOI BibTeX RDF
16	Qian Wang, Xiaoyu Song, William N. N. Hung, Ming Gu 0001, Jiaguang Sun 0001	Scalable Verification of a Generic End-Around-Carry Adder for Floating-Point Units by Coq.	IEEE Trans. Comput. Aided Des. Integr. Circuits Syst.	2015	DBLP DOI BibTeX RDF
16	Éric Tanter, Nicolas Tabareau	Gradual Certified Programming in Coq.	CoRR	2015	DBLP BibTeX RDF
16	Théo Zimmermann, Hugo Herbelin	Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant.	CoRR	2015	DBLP BibTeX RDF
16	Ali Assaf 0002, Raphaël Cauderlier	Mixing HOL and Coq in Dedukti (Extended Abstract).	PxTP@CADE	2015	DBLP DOI BibTeX RDF
16	Amin Timany, Bart Jacobs 0002	Category Theory in Coq 8.5.	CoRR	2015	DBLP BibTeX RDF
16	Jaap Boender, Florian Kammüller, Rajagopal Nagarajan	Formalization of Quantum Protocols using Coq.	QPL	2015	DBLP DOI BibTeX RDF
16	Bruno Barras, Carst Tankink, Enrico Tassi	Asynchronous processing of Coq documents: from the kernel up to the user interface.	CoRR	2015	DBLP BibTeX RDF
16	Floris van Doorn	Propositional Calculus in Coq.	CoRR	2015	DBLP BibTeX RDF
16	Sylvie Boldo, Catherine Lelay, Guillaume Melquiond	Coquelicot: A User-Friendly Library of Real Analysis for Coq.	Math. Comput. Sci.	2015	DBLP DOI BibTeX RDF
16	Yi Li 0010, Meng Sun 0002	Modeling and verification of component connectors in Coq.	Sci. Comput. Program.	2015	DBLP DOI BibTeX RDF
16	Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis	Mtac: A monad for typed tactic programming in Coq.	J. Funct. Program.	2015	DBLP DOI BibTeX RDF
16	Éric Tanter, Nicolas Tabareau	Gradual certified programming in Coq.	DLS	2015	DBLP DOI BibTeX RDF
16	Delphine Demange, David Pichardie, Léo Stefanesco	Verifying Fast and Sparse SSA-Based Optimizations in Coq.	CC	2015	DBLP DOI BibTeX RDF
16	Beta Ziliani, Matthieu Sozeau	A unification algorithm for Coq featuring universe polymorphism and overloading.	ICFP	2015	DBLP DOI BibTeX RDF
16	Christoph Benzmüller, Bruno Woltzenlogel Paleo	Interacting with Modal Logics in the Coq Proof Assistant.	CSR	2015	DBLP DOI BibTeX RDF
16	Stergios Chatzikyriakidis	Natural Language Reasoning using Coq: Interaction and Automation.	TALN	2015	DBLP BibTeX RDF
16	Mohammad-Mahdi Bidmeshki, Yiorgos Makris	VeriCoq: A Verilog-to-Coq converter for proof-carrying hardware automation.	ISCAS	2015	DBLP DOI BibTeX RDF
16	Fuli Zhou, Xu Wang, Chen Shan, Ni Lin	COQ math model case study for self-brand automobile industry.	IEEM	2015	DBLP DOI BibTeX RDF
16	Filip Sieczkowski, Ales Bizjak, Lars Birkedal	ModuRes: A Coq Library for Modular Reasoning About Concurrent Higher-Order Imperative Programming Languages.	ITP	2015	DBLP DOI BibTeX RDF
16	Petar Maksimovic, Alan Schmitt	HOCore in Coq.	ITP	2015	DBLP DOI BibTeX RDF
16	Bruno Barras, Carst Tankink, Enrico Tassi	Asynchronous Processing of Coq Documents: From the Kernel up to the User Interface.	ITP	2015	DBLP DOI BibTeX RDF
16	Steven Schäfer, Gert Smolka, Tobias Tebbi	Completeness and Decidability of de Bruijn Substitution Algebra in Coq.	CPP	2015	DBLP DOI BibTeX RDF
16	Jingyuan Cao, Ming Fu, Xinyu Feng 0001	Practical Tactics for Verifying C Programs in Coq.	CPP	2015	DBLP DOI BibTeX RDF
16	Richard Dapoigny, Patrick Barlatier	A Coq-Based Axiomatization of Tarski's Mereogeometry.	COSIT	2015	DBLP DOI BibTeX RDF
16	Théo Zimmermann, Hugo Herbelin	Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant.	CICM (Work in Progress)	2015	DBLP BibTeX RDF
16	Beta Ziliani	Interactive typed tactic programming in the Coq proof assistant.		2015	RDF
16	Nuno Gaspar, Ludovic Henrio, Eric Madelaine	Bringing Coq into the World of GCM Distributed Applications.	Int. J. Parallel Program.	2014	DBLP DOI BibTeX RDF
16	Pierre Castéran, Jacques Garrigue, David Nowak	Summer School on Coq (NII Shonan Meeting 2014-9).	NII Shonan Meet. Rep.	2014	DBLP BibTeX RDF
16	Hai Wan, Anping He, Zhiyang You, Xibin Zhao	Formal Proof of a Machine Closed Theorem in Coq.	J. Appl. Math.	2014	DBLP DOI BibTeX RDF
16	Qian Wang, Xiaoyu Song, Ming Gu 0001, Jia-Guang Sun 0001	Functional Verification of High Performance Adders in COQ.	J. Appl. Math.	2014	DBLP DOI BibTeX RDF
16	Jason Gross, Adam Chlipala, David I. Spivak	Experience Implementing a Performant Category-Theory Library in Coq.	CoRR	2014	DBLP BibTeX RDF
16	Carst Tankink	PIDE for Asynchronous Interaction with Coq.	UITP	2014	DBLP DOI BibTeX RDF
16	Parvez Mahmood Khan, M. M. Sufyan Beg	Measuring Cost of Quality (CoQ) on SDLC Projects is Indispensible for Effective Software Quality Assurance.	CoRR	2014	DBLP BibTeX RDF
16	Jónathan Heras, Ekaterina Komendantskaya	Proof Pattern Search in Coq/SSReflect.	CoRR	2014	DBLP BibTeX RDF
16	Cezary Kaliszyk, Lionel Mamane, Josef Urban	Machine Learning of Coq Proof Guidance: First Experiments.	CoRR	2014	DBLP BibTeX RDF
16	Jónathan Heras, Ekaterina Komendantskaya	HoTT formalisation in Coq: Dependency Graphs \& ML4PG.	CoRR	2014	DBLP BibTeX RDF
16	Christopher Meiklejohn	Vector Clocks in Coq: An Experience Report.	CoRR	2014	DBLP BibTeX RDF
16	Jónathan Heras, Ekaterina Komendantskaya	Recycling Proof Patterns in Coq: Case Studies.	Math. Comput. Sci.	2014	DBLP DOI BibTeX RDF
16	Stergios Chatzikyriakidis, Zhaohui Luo	Natural Language Inference in Coq.	J. Log. Lang. Inf.	2014	DBLP DOI BibTeX RDF
16	Thomas Braibant, Jacques-Henri Jourdan, David Monniaux	Implementing and Reasoning About Hash-consed Data Structures in Coq.	J. Autom. Reason.	2014	DBLP DOI BibTeX RDF
16	Julianna Zsido	Theorem of Three Circles in Coq.	J. Autom. Reason.	2014	DBLP DOI BibTeX RDF
16	Richard Dapoigny, Patrick Barlatier	Formalizing Context for Domain Ontologies in Coq.	Context in Computing	2014	DBLP DOI BibTeX RDF
16	Robbert Krebbers	Separation Algebras for C Verification in Coq.	VSTTE	2014	DBLP DOI BibTeX RDF
16	Jean-François Dufourd	Pointer Program Derivation Using Coq: Graphs and Schorr-Waite Algorithm.	ICFEM	2014	DBLP DOI BibTeX RDF
16	Beta Ziliani, Matthieu Sozeau	Towards a better-behaved unification algorithm for Coq.	UNIF	2014	DBLP BibTeX RDF
16	Gérard P. Huet, Hugo Herbelin	30 years of research and development around Coq.	POPL	2014	DBLP DOI BibTeX RDF
16	Cezary Kaliszyk, Lionel Mamane, Josef Urban	Machine Learning of Coq Proof Guidance: First Experiments.	SCSS	2014	DBLP DOI BibTeX RDF
16	Véronique Benzaken, Evelyne Contejean, Stefania Dumbrava	A Coq Formalization of the Relational Data Model.	ESOP	2014	DBLP DOI BibTeX RDF
16	Chao Li, Liang Dou, Zongyuan Yang	A metamodeling level transformation from UML sequence diagrams to Coq.	ICTCS	2014	DBLP BibTeX RDF
16	Richard Dapoigny, Patrick Barlatier	Specifying Well-Formed Part-Whole Relations in Coq.	ICCS	2014	DBLP DOI BibTeX RDF
16	Yoichi Hirai, Reynald Affeldt	What could Coq do for Database Software? - A Progress Report.	JFLA	2014	DBLP BibTeX RDF
16	Jean-Guillaume Dumas, Dominique Duval, Burak Ekici, Damien Pous	Formal verification in Coq of program properties involving the global state effect.	JFLA	2014	DBLP BibTeX RDF
16	Matthieu Sozeau, Nicolas Tabareau	Universe Polymorphism in Coq.	ITP	2014	DBLP DOI BibTeX RDF
16	Evmorfia-Iro Bartzia, Pierre-Yves Strub	A Formal Library for Elliptic Curves in the Coq Proof Assistant.	ITP	2014	DBLP DOI BibTeX RDF
16	Jason Gross, Adam Chlipala, David I. Spivak	Experience Implementing a Performant Category-Theory Library in Coq.	ITP	2014	DBLP DOI BibTeX RDF
16	Kento Emoto, Frédéric Loulergue, Julien Tesson	A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction.	ITP	2014	DBLP DOI BibTeX RDF
16	Robert Dockins	Formalized, Effective Domain Theory in Coq.	ITP	2014	DBLP DOI BibTeX RDF
16	Cyril Cohen, Anders Mörtberg	A Coq Formalization of Finitely Presented Modules.	ITP	2014	DBLP DOI BibTeX RDF
16	Christian Doczkal, Gert Smolka	Completeness and Decidability Results for CTL in Coq.	ITP	2014	DBLP DOI BibTeX RDF
16	Simon Robillard	Catamorphism Generation and Fusion Using Coq.	SYNASC	2014	DBLP DOI BibTeX RDF
16	Alberto Ciaffaglione, Ivan Scagnetto	Internal Adequacy of Bookkeeping in Coq.	LFMTP	2014	DBLP DOI BibTeX RDF
16	Washington de Carvalho Segundo, Flávio L. C. de Moura, Daniel Ventura	Formalizing a Named Explicit Substitutions Calculus in Coq.	CICM Workshops	2014	DBLP BibTeX RDF
16	Jónathan Heras, Thierry Coquand, Anders Mörtberg, Vincent Siles	Computing persistent homology within Coq/SSReflect.	ACM Trans. Comput. Log.	2013	DBLP DOI BibTeX RDF
16	Julianna Zsido	Theorem of three circles in Coq.	CoRR	2013	DBLP BibTeX RDF