Search results for "Coq"

Hits ?▲	Authors	Title	Venue	Year	Link
16	Thibault Hilaire, David Ilcinkas, Jérôme Leroux	A State-of-the-Art Karp-Miller Algorithm Certified in Coq.	TACAS (1)	2024	DBLP DOI BibTeX RDF
16	Andrew W. Appel, Ariel Kellison	VCFloat2: Floating-Point Error Analysis in Coq.	CPP	2024	DBLP DOI BibTeX RDF
16	Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard, Pierre-Marie Pédrot, Loïc Pujet	Martin-Löf à la Coq.	CPP	2024	DBLP DOI BibTeX RDF
16	Nicolas Chappe, Paul He, Ludovic Henrio, Yannick Zakowski, Steve Zdancewic	Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq.	Proc. ACM Program. Lang.	2023	DBLP DOI BibTeX RDF
16	Pedro Abreu, Benjamin Delaware, Alex Hubers, Christa Jenkins, J. Garrett Morris, Aaron Stump	A Type-Based Approach to Divide-and-Conquer Recursion in Coq.	Proc. ACM Program. Lang.	2023	DBLP DOI BibTeX RDF
16	David Nowak, Vlad Rusu	While Loops in Coq.	FROM	2023	DBLP DOI BibTeX RDF
16	Jason Gross, Andres Erbsen, Jade Philipoom, Rajashree Agrawal, Adam Chlipala	Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq.	CoRR	2023	DBLP DOI BibTeX RDF
16	Andrei Aleksandrov, Kim Völlinger	Formalizing Piecewise Affine Activation Functions of Neural Networks in Coq.	CoRR	2023	DBLP DOI BibTeX RDF
16	Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard, Pierre-Marie Pédrot, Loïc Pujet	Martin-Löf à la Coq.	CoRR	2023	DBLP DOI BibTeX RDF
16	Nadeem Abdul Hamid	(Nearest) Neighbors You Can Rely On: Formally Verified k-d Tree Construction and Search in Coq.	CoRR	2023	DBLP DOI BibTeX RDF
16	Zachary Flores, Angelo Taranto, Eric Bond, Yakir Forman	A Formalization of Operads in Coq.	CoRR	2023	DBLP DOI BibTeX RDF
16	Maria J. D. Lima, Flávio L. C. de Moura	A Formalized Extension of the Substitution Lemma in Coq.	FROM	2023	DBLP DOI BibTeX RDF
16	Xinyi Wan, Ke Xu, Qinxiang Cao	Coq Formalization of ZFC Set Theory for Teaching Scenarios.	Int. J. Softw. Informatics	2023	DBLP DOI BibTeX RDF
16	Dominik Kirst, Marc Hermes	Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq.	J. Autom. Reason.	2023	DBLP DOI BibTeX RDF
16	Érik Martin-Dorel, Guillaume Melquiond, Pierre Roux	Enabling Floating-Point Arithmetic in the Coq Proof Assistant.	J. Autom. Reason.	2023	DBLP DOI BibTeX RDF
16	Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Carmine Abate, Nikolaj Sidorenco, Catalin Hritcu, Kenji Maillard, Bas Spitters	SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq.	ACM Trans. Program. Lang. Syst.	2023	DBLP DOI BibTeX RDF
16	Jonathan Chan, Yufeng Li, William J. Bowman	Is sized typing for Coq practical?	J. Funct. Program.	2023	DBLP DOI BibTeX RDF
16	Olivier Danvy	Fold-unfold lemmas for reasoning about recursive programs using the Coq proof assistant - ERRATUM.	J. Funct. Program.	2023	DBLP DOI BibTeX RDF
16	ZhengPu Shi, GuoJun Xie, Gang Chen	CoqMatrix: Formal matrix library with multiple models in Coq.	J. Syst. Archit.	2023	DBLP DOI BibTeX RDF
16	Frédéric Loulergue, Jolan Philippe	Towards Verified Scalable Parallel Computing with Coq and Spark.	FTfJP@ECOOP	2023	DBLP DOI BibTeX RDF
16	Haniel Barbosa, Chantal Keller, Andrew Reynolds 0001, Arjun Viswanathan, Cesare Tinelli, Clark W. Barrett	An Interactive SMT Tactic in Coq using Abductive Reasoning.	LPAR	2023	DBLP DOI BibTeX RDF
16	Jan Tusil, Péter Bereczky, Dániel Horpácsi	Interactive Matching Logic Proofs in Coq.	ICTAC	2023	DBLP DOI BibTeX RDF
16	Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero, Houda Mouhcine	A Coq Formalization of Lebesgue Induction Principle and Tonelli's Theorem.	FM	2023	DBLP DOI BibTeX RDF
16	Rundong Mu, Qin Li	A Coq Implementation of the Program Algebra in Jifeng He's New Roadmap for Linking Theories of Programming.	Theories of Programming and Formal Methods	2023	DBLP DOI BibTeX RDF
16	Ayumu Saito, Reynald Affeldt	Experimenting with an Intrinsically-Typed Probabilistic Programming Language in Coq.	APLAS	2023	DBLP DOI BibTeX RDF
16	Giorgio Audrito, Daniel Haures	Combining Static and Runtime Verification with AC and Coq.	VORTEX@ISSTA	2023	DBLP DOI BibTeX RDF
16	Xupeng Li, Xuheng Li, Wei Qiang, Ronghui Gu, Jason Nieh	Spoq: Scaling Machine-Checkable Systems Verification in Coq.	OSDI	2023	DBLP BibTeX RDF
16	Dominique Larchey-Wendling, Jean-François Monin	Proof Pearl: Faithful Computation and Extraction of μ-Recursive Algorithms in Coq.	ITP	2023	DBLP DOI BibTeX RDF
16	Ana de Almeida Borges, Annalí Casanueva Artís, Jean-Rémy Falleri, Emilio Jesús Gallego Arias, Érik Martin-Dorel, Karl Palmskog, Alexander Serebrenik, Théo Zimmermann	Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users.	ITP	2023	DBLP DOI BibTeX RDF
16	Pierre Pomeret-Coquot, Hélène Fargier, Érik Martin-Dorel	Bel-Games: A Formal Theory of Games of Incomplete Information Based on Belief Functions in the Coq Proof Assistant.	ITP	2023	DBLP DOI BibTeX RDF
16	Reynald Affeldt, Cyril Cohen, Ayumu Saito	Semantics of Probabilistic Programs using s-Finite Kernels in Coq.	CPP	2023	DBLP DOI BibTeX RDF
16	Benjamin Grégoire, Jean-Christophe Léchenet, Enrico Tassi	Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin's Data Types with Coq-Elpi.	CPP	2023	DBLP DOI BibTeX RDF
16	Eske Hoy Nielsen, Danil Annenkov, Bas Spitters	Formalising Decentralised Exchanges in Coq.	CPP	2023	DBLP DOI BibTeX RDF
16	Andrei Aleksandrov, Kim Völlinger	Formalizing Piecewise Affine Activation Functions of Neural Networks in Coq.	NFM	2023	DBLP DOI BibTeX RDF
16	Yannick Forster 0002, Felix Jahn	Constructive and Synthetic Reducibility Degrees: Post's Problem for Many-One and Truth-Table Reducibility in Coq.	CSL	2023	DBLP DOI BibTeX RDF
16	Burak Ekici, Arjun Viswanathan, Yoni Zohar, Cesare Tinelli, Clark W. Barrett	Formal Verification of Bit-Vector Invertibility Conditions in Coq.	FroCoS	2023	DBLP DOI BibTeX RDF
16	Véronique Benzaken, Evelyne Contejean, Mohammed Houssem Hachmaoui, Chantal Keller, Louis Mandel, Avraham Shinnar, Jérôme Siméon	Translating canonical SQL to imperative code in Coq.	Proc. ACM Program. Lang.	2022	DBLP DOI BibTeX RDF
16	Vlad Rusu, David Nowak	Defining Corecursive Functions in Coq Using Approximations (Artifact).	Dagstuhl Artifacts Ser.	2022	DBLP DOI BibTeX RDF
16	Sylvie Boldo, François Clément, Louise Leclerc	A Coq Formalization of the Bochner integral.	CoRR	2022	DBLP BibTeX RDF
16	Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero, Houda Mouhcine	Lebesgue Induction and Tonelli's Theorem in Coq.	CoRR	2022	DBLP BibTeX RDF
16	Péter Bereczky, Xiaohong Chen 0002, Dániel Horpácsi, Tamás Bálint Mizsei, Lucas Peña, Jan Tusil	Mechanizing Matching Logic in Coq.	FROM	2022	DBLP DOI BibTeX RDF
16	Catherine Dubois, Nicolas Magaud, Alain Giorgetti	Pragmatic isomorphism proofs between Coq representations: application to lambda-term families.	CoRR	2022	DBLP DOI BibTeX RDF
16	Karl Palmskog, Enrico Tassi, Théo Zimmermann	Reliably Reproducing Machine-Checked Proofs with the Coq Platform.	CoRR	2022	DBLP DOI BibTeX RDF
16	Jason Gross, Théo Zimmermann, Miraya Poddar-Agrawal, Adam Chlipala	Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq.	CoRR	2022	DBLP BibTeX RDF
16	Véronique Benzaken, Evelyne Contejean, Mohammed Houssem Hachmaoui, Chantal Keller, Louis Mandel, Avraham Shinnar, Jérôme Siméon	Translating Canonical SQL to Imperative Code in Coq.	CoRR	2022	DBLP DOI BibTeX RDF
16	Ana de Almeida Borges	Towards a Coq formalization of a quantified modal logic.	CoRR	2022	DBLP DOI BibTeX RDF
16	Eske Hoy Nielsen, Danil Annenkov, Bas Spitters	Formalising Decentralised Exchanges in Coq.	CoRR	2022	DBLP DOI BibTeX RDF
16	Ana de Almeida Borges, Mireia González Bedmar, Juan José Conejero Rodríguez, Eduardo Hermo Reyes, Joaquim Casals Buñuel, Joost J. Joosten	FV Time: a formally verified Coq library.	CoRR	2022	DBLP DOI BibTeX RDF
16	Nicolas Chappe, Paul He, Ludovic Henrio, Yannick Zakowski, Steve Zdancewic	Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq.	CoRR	2022	DBLP DOI BibTeX RDF
16	Dominique Larchey-Wendling, Yannick Forster 0002	Hilbert's Tenth Problem in Coq (Extended Version).	Log. Methods Comput. Sci.	2022	DBLP DOI BibTeX RDF
16	Dominik Kirst, Dominique Larchey-Wendling	Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens.	Log. Methods Comput. Sci.	2022	DBLP DOI BibTeX RDF
16	Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero	A Coq Formalization of Lebesgue Integration of Nonnegative Functions.	J. Autom. Reason.	2022	DBLP DOI BibTeX RDF
16	Olivier Danvy	Fold-unfold lemmas for reasoning about recursive programs using the Coq proof assistant.	J. Funct. Program.	2022	DBLP DOI BibTeX RDF
16	Avraham Shinnar, Barry M. Trager	General Probability in Coq.	DSN Workshops	2022	DBLP DOI BibTeX RDF
16	Jérôme Hugues, Lutz Wrage, John Hatcliff, Danielle Stewart	Mechanization of a Large DSML: An Experiment with AADL and Coq.	MEMOCODE	2022	DBLP DOI BibTeX RDF
16	Joshua M. Cohen, Qinshi Wang, Andrew W. Appel	Verified Erasure Correction in Coq with MathComp and VST.	CAV (2)	2022	DBLP DOI BibTeX RDF
16	Felipe Lisboa Malaquias, Mihail Asavoae, Florian Brandner	A Coq Framework for More Trustworthy DRAM Controllers.	RTNS	2022	DBLP DOI BibTeX RDF
16	Ayumu Saito, Reynald Affeldt	Towards a Practical Library for Monadic Equational Reasoning in Coq.	MPC	2022	DBLP DOI BibTeX RDF
16	Ariel Agne Da Silveira, Rodrigo Ribeiro, Miguel Alfredo Nunes, Paulo Torrens, Karina Girardi Roggia	A Sound Deep Embedding of Arbitrary Normal Modal Logics in Coq.	SBLP	2022	DBLP DOI BibTeX RDF
16	Catherine Dubois, Nicolas Magaud, Alain Giorgetti	Pragmatic Isomorphism Proofs Between Coq Representations: Application to Lambda-Term Families.	TYPES	2022	DBLP DOI BibTeX RDF
16	Vlad Rusu, David Nowak	Defining Corecursive Functions in Coq Using Approximations.	ECOOP	2022	DBLP DOI BibTeX RDF
16	Ana de Almeida Borges	Towards a Coq Formalization of a Quantified Modal Logic.	ARQNL@IJCAR	2022	DBLP BibTeX RDF
16	Kimaya Bedarkar, Mariam Vardishvili, Sergey Bozhko, Marco Maida, Björn B. Brandenburg	From Intuition to Coq: A Case Study in Verified Response-Time Analysis 1 of FIFO Scheduling.	RTSS	2022	DBLP DOI BibTeX RDF
16	Conor Reynolds, Rosemary Monahan	Machine-Assisted Proofs for Institutions in Coq.	IFM	2022	DBLP DOI BibTeX RDF
16	Nicolas Magaud	Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3, 2) Using the Coq Proof Assistant.	ITP	2022	DBLP DOI BibTeX RDF
16	Malgorzata Biernacka, Witold Charatonik, Tomasz Drab	The Zoo of Lambda-Calculus Reduction Strategies, And Coq.	ITP	2022	DBLP DOI BibTeX RDF
16	Johannes Hostert, Andrej Dudenhefner, Dominik Kirst	Undecidability of Dyadic First-Order Logic in Coq.	ITP	2022	DBLP DOI BibTeX RDF
16	Jason Gross, Théo Zimmermann, Miraya Poddar-Agrawal, Adam Chlipala	Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq.	ITP	2022	DBLP DOI BibTeX RDF
16	Yannick Forster 0002, Fabian Kunze, Nils Lauermann	Synthetic Kolmogorov Complexity in Coq.	ITP	2022	DBLP DOI BibTeX RDF
16	Yichen Tao, Qinxiang Cao	LOGIC: A Coq Library for Logics.	SETTA	2022	DBLP DOI BibTeX RDF
16	ZhengPu Shi, Gang Chen	Integration of Multiple Formal Matrix Models in Coq.	SETTA	2022	DBLP DOI BibTeX RDF
16	Dan Frumin	Semantic cut elimination for the logic of bunched implications, formalized in Coq.	CPP	2022	DBLP DOI BibTeX RDF
16	Mark Koch, Dominik Kirst	Undecidability, incompleteness, and completeness of second-order logic in Coq.	CPP	2022	DBLP DOI BibTeX RDF
16	Andrew W. Appel	Coq's vibrant ecosystem for verification engineering (invited talk).	CPP	2022	DBLP DOI BibTeX RDF
16	Conor Reynolds, Rosemary Monahan	Machine-Assisted Proofs for Institutions in Coq.	TASE	2022	DBLP DOI BibTeX RDF
16	Wenjun Shi, Qinxiang Cao, Yuxin Deng, Hanru Jiang, Yuan Feng 0001	Symbolic Reasoning About Quantum Circuits in Coq.	J. Comput. Sci. Technol.	2021	DBLP DOI BibTeX RDF
16	Yezhou Liu, Radu Nicolescu, Jing Sun 0002	Formal verification of cP systems using Coq.	J. Membr. Comput.	2021	DBLP DOI BibTeX RDF
16	Luís Cruz-Filipe, Fabrizio Montesi, Marco Peressotti	Formalising a Turing-Complete Choreographic Language in Coq.	CoRR	2021	DBLP BibTeX RDF
16	François Clément, Vincent Martin	Lebesgue integration. Detailed proofs to be formalized in Coq.	CoRR	2021	DBLP BibTeX RDF
16	Deivid Vale, Niels van der Weide	Formalizing Higher-Order Termination in Coq.	CoRR	2021	DBLP BibTeX RDF
16	Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero	A Coq Formalization of Lebesgue Integration of Nonnegative Functions.	CoRR	2021	DBLP BibTeX RDF
16	Elizabeth Dietrich	A beginner guide to Iris, Coq and separation logic.	CoRR	2021	DBLP BibTeX RDF
16	Dan Frumin	Semantic Cut Elimination for the Logic of Bunched Implications, Formalized in Coq.	CoRR	2021	DBLP BibTeX RDF
16	Liao Zhang, Lasse Blaauwbroek, Bartosz Piotrowski, Prokop Cerný, Cezary Kaliszyk, Josef Urban	Online Machine Learning Techniques for Coq: A Comparison.	CoRR	2021	DBLP BibTeX RDF
16	Nicolas Magaud	Integrating an Automated Prover for Projective Geometry as a New Tactic in the Coq Proof Assistant.	PxTP	2021	DBLP DOI BibTeX RDF
16	Laila El-Beheiry, Giselle Reis, Ammar Karkour	SMLtoCoq: Automated Generation of Coq Specifications and Proof Obligations from SML Programs with Contracts.	LFMTP	2021	DBLP DOI BibTeX RDF
16	Dominik Kirst, Dominique Larchey-Wendling	Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens.	CoRR	2021	DBLP BibTeX RDF
16	Valentin Blot, Louise Dubois de Prisque, Chantal Keller, Pierre Vial	General Automation in Coq through Modular Transformations.	PxTP	2021	DBLP DOI BibTeX RDF
16	Pengyu Nie 0001, Karl Palmskog, Junyi Jessy Li, Milos Gligoric 0001	Roosterize: Suggesting Lemma Names for Coq Verification Projects Using Deep Learning.	CoRR	2021	DBLP BibTeX RDF
16	Bruno Bernardo, Raphaël Cauderlier, Guillaume Claret, Arvid Jakobsson, Basile Pesin, Julien Tesson	Making Tezos smart contracts more reliable with Coq.	CoRR	2021	DBLP BibTeX RDF
16	Florian Steinberg 0001, Laurent Théry, Holger Thies	Computable analysis and notions of continuity in Coq.	Log. Methods Comput. Sci.	2021	DBLP BibTeX RDF
16	Carmine Abate, Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Catalin Hritcu, Kenji Maillard, Bas Spitters	SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq.	IACR Cryptol. ePrint Arch.	2021	DBLP BibTeX RDF
16	Peter Schwabe, Benoît Viguier, Timmy Weerwag, Freek Wiedijk	A Coq proof of the correctness of X25519 in TweetNaCl.	IACR Cryptol. ePrint Arch.	2021	DBLP BibTeX RDF
16	Guillaume Ambal, Sergueï Lenglet, Alan Schmitt	HOπ in Coq.	J. Autom. Reason.	2021	DBLP DOI BibTeX RDF
16	Raul Fervari, Francisco Trucco, Beta Ziliani	Verification of dynamic bisimulation theorems in Coq.	J. Log. Algebraic Methods Program.	2021	DBLP DOI BibTeX RDF
16	Gustavo Carvalho, Igor Meira	Validating, verifying and testing timed data-flow reactive systems in Coq from controlled natural-language requirements.	Sci. Comput. Program.	2021	DBLP DOI BibTeX RDF
16	Joachim Breitner, Antal Spector-Zabusky, Yao Li 0004, Christine Rizkallah, John Wiegley, Joshua M. Cohen, Stephanie Weirich	Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code.	J. Funct. Program.	2021	DBLP DOI BibTeX RDF
16	Daniel Britten, Vilhelm Sjöberg, Steve Reeves	Using Coq to Enforce the Checks-Effects-Interactions Pattern in DeepSEA Smart Contracts (Short Paper).	FMBC@CAV	2021	DBLP DOI BibTeX RDF
16	Akira Tanaka	Coq to C translation with partial evaluation.	PEPM@POPL	2021	DBLP DOI BibTeX RDF
16	Xiaokun Luan, Xiyue Zhang, Meng Sun 0002	Using LSTM to Predict Tactics in Coq.	SEKE	2021	DBLP DOI BibTeX RDF