Search results for "Coq"

Hits ?▲	Authors	Title	Venue	Year	Link
16	Jónathan Heras, Ekaterina Komendantskaya	ML4PG: proof-mining in Coq	CoRR	2013	DBLP BibTeX RDF
16	Jan Olaf Blech, Sidi Ould Biha	On Formal Reasoning on the Semantics of PLC using Coq	CoRR	2013	DBLP BibTeX RDF
16	Thomas Braibant, Jacques-Henri Jourdan, David Monniaux	Implementing and reasoning about hash-consed data structures in Coq.	CoRR	2013	DBLP BibTeX RDF
16	Jeremy Avigad, Krzysztof Kapulkin, Peter LeFanu Lumsdaine	Homotopy limits in Coq	CoRR	2013	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.	CoRR	2013	DBLP BibTeX RDF
16	Lionel Rieg	Extracting Herbrand trees from Coq	CoRR	2013	DBLP BibTeX RDF
16	Jónathan Heras, Ekaterina Komendantskaya	Statistical Proof-Patterns in Coq/SSReflect	CoRR	2013	DBLP BibTeX RDF
16	Damien Pous	Kleene Algebra with Tests and Coq Tools for While Programs	CoRR	2013	DBLP BibTeX RDF
16	Thomas Braibant, Jacques-Henri Jourdan, David Monniaux	Implementing hash-consed structures in Coq	CoRR	2013	DBLP BibTeX RDF
16	Makarius Wenzel	PIDE as front-end technology for Coq	CoRR	2013	DBLP BibTeX RDF
16	Adam Chlipala	Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant.		2013	RDF
16	Dongxi Liu, Neale Leslie Fulton, John Zic, Martin de Groot	Verifying an Aircraft Proximity Characterization Method in Coq.	ICFEM	2013	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.	ICFP	2013	DBLP DOI BibTeX RDF
16	Pierre Courtieu, Maria-Virginia Aponte, Tristan Crolard, Zhi Zhang, Robby, Jason Belt, John Hatcliff, Jérôme Guitton, Trevor Jennings	Towards the formalization of SPARK 2014 semantics with explicit run-time checks using coq.	HILT	2013	DBLP DOI BibTeX RDF
16	Nada Habli, Amy P. Felty	Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs.	PxTP@CADE	2013	DBLP DOI BibTeX RDF
16	Richard Dapoigny, Patrick Barlatier	Modeling Ontological Structures with Type Classes in Coq.	ICCS	2013	DBLP DOI BibTeX RDF
16	Hendrik Tews	Formalizing Cut Elimination of Coalgebraic Logics in Coq.	TABLEAUX	2013	DBLP DOI BibTeX RDF
16	Jael Kriener, Andy King, Sandrine Blazy	Proofs you can believe in: proving equivalences between Prolog semantics in Coq.	PPDP	2013	DBLP DOI BibTeX RDF
16	Wojciech Jedynak, Malgorzata Biernacka, Dariusz Biernacki	An operational foundation for the tactic language of Coq.	PPDP	2013	DBLP DOI BibTeX RDF
16	Andrew Kennedy, Nick Benton, Jonas Braband Jensen, Pierre-Évariste Dagand	Coq: the world's best macro assembler?	PPDP	2013	DBLP DOI BibTeX RDF
16	Yi Li 0010, Meng Sun 0002	Modeling and Analysis of Component Connectors in Coq.	FACS	2013	DBLP DOI BibTeX RDF
16	Frédéric Loulergue, Virginia Niculescu, Simon Robillard	Powerlists in Coq: Programming and Reasoning.	CANDAR	2013	DBLP DOI BibTeX RDF
16	Cyril Cohen	Pragmatic Quotient Types in Coq.	ITP	2013	DBLP DOI BibTeX RDF
16	Jörg Endrullis, Dimitri Hendriks, Martin Bodin	Circular Coinduction in Coq Using Bisimulation-Up-To Techniques.	ITP	2013	DBLP DOI BibTeX RDF
16	Assia Mahboubi, Enrico Tassi	Canonical Structures for the Working Coq User.	ITP	2013	DBLP DOI BibTeX RDF
16	Thomas Braibant, Jacques-Henri Jourdan, David Monniaux	Implementing Hash-Consed Structures in Coq.	ITP	2013	DBLP DOI BibTeX RDF
16	Evgeny Makarov, Bas Spitters	The Picard Algorithm for Ordinary Differential Equations in Coq.	ITP	2013	DBLP DOI BibTeX RDF
16	Damien Pous	Kleene Algebra with Tests and Coq Tools for while Programs.	ITP	2013	DBLP DOI BibTeX RDF
16	Robbert Krebbers	Aliasing Restrictions of C11 Formalized in Coq.	CPP	2013	DBLP DOI BibTeX RDF
16	Christian Doczkal, Jan-Oliver Kaiser, Gert Smolka	A Constructive Theory of Regular Languages in Coq.	CPP	2013	DBLP DOI BibTeX RDF
16	Gordon Stewart 0001	Computational Verification of Network Programs in Coq.	CPP	2013	DBLP DOI BibTeX RDF
16	Érik Martin-Dorel, Laurence Rideau, Laurent Théry, Micaela Mayero, Ioana Pasca	Certified, Efficient and Sharp Univariate Taylor Models in COQ.	SYNASC	2013	DBLP DOI BibTeX RDF
16	Ken Madlener, Sjaak Smetsers	GSOS Formalized in Coq.	TASE	2013	DBLP DOI BibTeX RDF
16	Nicolas Magaud, Julien Narboux, Pascal Schreck	A case study in formalizing projective geometry in Coq: Desargues theorem.	Comput. Geom.	2012	DBLP DOI BibTeX RDF
16	Christophe Brun, Jean-François Dufourd, Nicolas Magaud	Designing and proving correct a convex hull algorithm with hypermaps in Coq.	Comput. Geom.	2012	DBLP DOI BibTeX RDF
16	Thomas Braibant, Damien Pous	Deciding Kleene Algebras in Coq	Log. Methods Comput. Sci.	2012	DBLP DOI BibTeX RDF
16	Jónathan Heras, Thierry Coquand, Anders Mörtberg, Vincent Siles	Computing Persistent Homology within Coq/SSReflect	CoRR	2012	DBLP BibTeX RDF
16	Frédéric Blanqui, Adam Koprowski	CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates.	CoRR	2012	DBLP BibTeX RDF
16	Nick Benton, Chung-Kil Hur, Andrew Kennedy, Conor McBride	Strongly Typed Term Representations in Coq.	J. Autom. Reason.	2012	DBLP DOI BibTeX RDF
16	André Hirschowitz, Marco Maggesi	Nested Abstract Syntax in Coq.	J. Autom. Reason.	2012	DBLP DOI BibTeX RDF
16	Guillaume Melquiond	Floating-point arithmetic in the Coq system.	Inf. Comput.	2012	DBLP DOI BibTeX RDF
16	Christophe Brun, Jean-François Dufourd, Nicolas Magaud	Formal Proof in Coq and Derivation of an Imperative Program to Compute Convex Hulls.	Automated Deduction in Geometry	2012	DBLP DOI BibTeX RDF
16	Nelma Moreira, David Pereira, Simão Melo de Sousa	Deciding Regular Expressions (In-)Equivalence in Coq.	RAMiCS	2012	DBLP DOI BibTeX RDF
16	Pierre-Yves Strub, Nikhil Swamy, Cédric Fournet, Juan Chen 0002	Self-certification: bootstrapping certified typecheckers in F* with Coq.	POPL	2012	DBLP DOI BibTeX RDF
16	Vladimir Komendantsky	Reflexive toolbox for regular expression matching: verification of functional programs in Coq+Ssreflect.	PLPV	2012	DBLP DOI BibTeX RDF
16	Julian Mackay, Hannes Mehnert, Alex Potanin, Lindsay Groves, Nicholas Cameron 0001	Encoding Featherweight Java with assignment and immutability using the Coq proof assistant.	FTfJP@ECOOP	2012	DBLP DOI BibTeX RDF
16	Dimitur Nikolaev Krustev	Towards a Framework for Building Formally Verified Supercompilers in Coq.	Trends in Functional Programming	2012	DBLP DOI BibTeX RDF
16	Reynald Affeldt, Manabu Hagiwara	Formalization of Shannon's Theorems in SSReflect-Coq.	ITP	2012	DBLP DOI BibTeX RDF
16	Cyril Cohen	Construction of Real Algebraic Numbers in Coq.	ITP	2012	DBLP DOI BibTeX RDF
16	Jesper Bengtson, Jonas Braband Jensen, Lars Birkedal	Charge! - A Framework for Higher-Order Separation Logic in Coq.	ITP	2012	DBLP DOI BibTeX RDF
16	Marino Miculan, Marco Paviotti	Synthesis of Distributed Mobile Programs Using Monadic Types in Coq.	ITP	2012	DBLP DOI BibTeX RDF
16	Maxime Dénès, Anders Mörtberg, Vincent Siles	A Refinement-Based Approach to Computational Algebra in Coq.	ITP	2012	DBLP DOI BibTeX RDF
16	Raymond McCarthy Bergeron	La lune et le coq.	SIGGRAPH Computer Animation Festival	2012	DBLP DOI BibTeX RDF
16	Sylvie Boldo, Catherine Lelay, Guillaume Melquiond	Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives.	CPP	2012	DBLP DOI BibTeX RDF
16	Nicolas Brisebarre, Mioara Joldes, Érik Martin-Dorel, Micaela Mayero, Jean-Michel Muller, Ioana Pasca, Laurence Rideau, Laurent Théry	Rigorous Polynomial Approximation Using Taylor Models in Coq.	NASA Formal Methods	2012	DBLP DOI BibTeX RDF
16	Wouter Swierstra	xmonad in Coq (experience report): programming a window manager in a proof assistant.	Haskell	2012	DBLP DOI BibTeX RDF
16	Jesse Alama, Lionel Mamane, Josef Urban	Dependencies in Formal Mathematics: Applications and Extraction for Coq and Mizar.	AISC/MKM/Calculemus	2012	DBLP DOI BibTeX RDF
16	Hai Wan, Gang Chen 0004, Xiaoyu Song, Ming Gu 0001	Formalisation and verification of programmable logic controllers timers in Coq.	IET Softw.	2011	DBLP DOI BibTeX RDF
16	Frédéric Blanqui, Adam Koprowski	CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates.	Math. Struct. Comput. Sci.	2011	DBLP DOI BibTeX RDF
16	Nassima Izerrouken, Marc Pantel, Xavier Thirioux, Olivier Ssi Yan Kai	Expérimentations en Coq pour un générateur de code qualifiable.	Tech. Sci. Informatiques	2011	DBLP DOI BibTeX RDF
16	César Domínguez 0001, Julio Rubio 0001	Effective homology of bicomplexes, formalized in Coq.	Theor. Comput. Sci.	2011	DBLP DOI BibTeX RDF
16	Benedikt Ahrens, Julianna Zsido	Initial Semantics for higher-order typed syntax in Coq.	J. Formaliz. Reason.	2011	DBLP DOI BibTeX RDF
16	Thomas Braibant, Damien Pous	Tactics for Reasoning modulo AC in Coq	CoRR	2011	DBLP BibTeX RDF
16	Thomas Braibant	Coquet: a Coq library for verifying hardware	CoRR	2011	DBLP BibTeX RDF
16	Robbert Krebbers, Bas Spitters	Type classes for efficient exact real arithmetic in Coq	Log. Methods Comput. Sci.	2011	DBLP DOI BibTeX RDF
16	Jan Olaf Blech	A Tool for the Certification of PLCs based on a Coq Semantics for Sequential Function Charts	CoRR	2011	DBLP BibTeX RDF
16	Robbert Krebbers, Bas Spitters	Computer certified efficient exact reals in Coq	CoRR	2011	DBLP BibTeX RDF
16	Emmanuel Polonowski	Generic Environments in Coq	CoRR	2011	DBLP BibTeX RDF
16	Stéphane Lescuyer	First-Class Containers in Coq.	Stud. Inform. Univ.	2011	DBLP BibTeX RDF
16	Christine Paulin-Mohring	Introduction to the Coq Proof-Assistant for Practical Software Verification.	LASER Summer School	2011	DBLP DOI BibTeX RDF
16	Sylvie Boldo, Guillaume Melquiond	Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq.	IEEE Symposium on Computer Arithmetic	2011	DBLP DOI BibTeX RDF
16	Aloïs Brunel	Non-constructive complex analysis in Coq.	TYPES	2011	DBLP DOI BibTeX RDF
16	Sidi Ould Biha	A Formal Semantics of PLC Programs in Coq.	COMPSAC	2011	DBLP DOI BibTeX RDF
16	Jesper Bengtson, Jonas Braband Jensen, Filip Sieczkowski, Lars Birkedal	Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq.	ITP	2011	DBLP DOI BibTeX RDF
16	Anne-Gwenn Bosser, Pierre Courtieu, Julien Forest, Marc Cavazza	Structural Analysis of Narratives with the Coq Proof Assistant.	ITP	2011	DBLP DOI BibTeX RDF
16	Tuan-Minh Pham, Yves Bertot, Julien Narboux	A Coq-Based Library for Interactive and Automated Theorem Proving in Plane Geometry.	ICCSA (4)	2011	DBLP DOI BibTeX RDF
16	Martin Henz, Aquinas Hobor	Teaching Experience: Logic and Formal Methods with Coq.	CPP	2011	DBLP DOI BibTeX RDF
16	Thomas Braibant	Coquet: A Coq Library for Verifying Hardware.	CPP	2011	DBLP DOI BibTeX RDF
16	Thomas Braibant, Damien Pous	Tactics for Reasoning Modulo AC in Coq.	CPP	2011	DBLP DOI BibTeX RDF
16	Michaël Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry, Benjamin Werner	A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses.	CPP	2011	DBLP DOI BibTeX RDF
16	Frédéric Besson, Pierre-Emmanuel Cornilleau, David Pichardie	Modular SMT Proofs for Fast Reflexive Checking Inside Coq.	CPP	2011	DBLP DOI BibTeX RDF
16	Jieung Kim, Sukyoung Ryu	Coq Mechanization of Featherweight Fortress with Multiple Dispatch and Multiple Inheritance.	CPP	2011	DBLP DOI BibTeX RDF
16	Jean-David Génevaux, Julien Narboux, Pascal Schreck	Formalization of Wu's Simple Method in Coq.	CPP	2011	DBLP DOI BibTeX RDF
16	Jan Olaf Blech, Sidi Ould Biha	Verification of PLC Properties Based on Formal Semantics in Coq.	SEFM	2011	DBLP DOI BibTeX RDF
16	Kosuke Ono, Yoichi Hirai, Yoshinori Tanabe, Natsuko Noda, Masami Hagiya	Using Coq in Specification and Program Extraction of Hadoop MapReduce Applications.	SEFM	2011	DBLP DOI BibTeX RDF
16	Robbert Krebbers, Bas Spitters	Computer Certified Efficient Exact Reals in Coq.	Calculemus/MKM	2011	DBLP DOI BibTeX RDF
16	Vladimir Komendantsky, Alexander Konovalov 0001, Steve Linton	View of Computer Algebra Data from Coq.	Calculemus/MKM	2011	DBLP DOI BibTeX RDF
16	Jónathan Heras, María Poza, Maxime Dénès, Laurence Rideau	Incidence Simplicial Matrices Formalized in Coq/SSReflect.	Calculemus/MKM	2011	DBLP DOI BibTeX RDF
16	Robbert Krebbers, Freek Wiedijk	A Formalization of the C99 Standard in HOL, Isabelle and Coq.	Calculemus/MKM	2011	DBLP DOI BibTeX RDF
16	Hermann Lehner	A formal definition of JML in Coq and its application to runtime assertion checking.		2011	RDF
16	Vladimir Komendantsky, Alexander Konovalov 0001, Steve Linton	Interfacing Coq + SSReflect with GAP.	UITP	2010	DBLP DOI BibTeX RDF
16	Gang Chen	Formalization of a Parameterized Parallel Adder Within the Coq Theorem Prover.	IEEE Trans. Comput. Aided Des. Integr. Circuits Syst.	2010	DBLP DOI BibTeX RDF
16	Georges Gonthier, Assia Mahboubi	An introduction to small scale reflection in Coq.	J. Formaliz. Reason.	2010	DBLP DOI BibTeX RDF
16	José Grimm	Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets.	J. Formaliz. Reason.	2010	DBLP DOI BibTeX RDF
16	Adam Chlipala	An Introduction to Programming and Proving with Dependent Types in Coq.	J. Formaliz. Reason.	2010	DBLP DOI BibTeX RDF
16	Loïc Pottier	Connecting Gröbner Bases Programs with Coq to do Proofs in Algebra, Geometry and Arithmetics	CoRR	2010	DBLP BibTeX RDF
16	César Domínguez 0001, Julio Rubio 0001	Computing in Coq with Infinite Algebraic Data Structures	CoRR	2010	DBLP BibTeX RDF
16	Christine Choppy, Micaela Mayero, Laure Petrucci	Coloured Petri net refinement specification and correctness proof with Coq.	Innov. Syst. Softw. Eng.	2010	DBLP DOI BibTeX RDF
16	Laurent Fuchs, Laurent Théry	A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry.	Automated Deduction in Geometry	2010	DBLP DOI BibTeX RDF
16	Filip Sieczkowski, Malgorzata Biernacka, Dariusz Biernacki	Automating Derivations of Abstract Machines from Reduction Semantics: - A Generic Formalization of Refocusing in Coq.	IFL	2010	DBLP DOI BibTeX RDF