Search results for "coq"

Hits ?▲	Authors	Title	Venue	Year	Link
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.	CSF	2021	DBLP DOI BibTeX RDF
16	Peter Schwabe, Benoît Viguier, Timmy Weerwag, Freek Wiedijk	A Coq proof of the correctness of X25519 in TweetNaCl.	CSF	2021	DBLP DOI BibTeX RDF
16	Xiaokun Luan, Meng Sun 0002	Modeling and Verification of CKB Consensus Protocol in Coq.	QRS Companion	2021	DBLP DOI BibTeX RDF
16	Dominique Larchey-Wendling	Synthetic Undecidability of MSELL via FRACTRAN Mechanised in Coq.	FSCD	2021	DBLP DOI BibTeX RDF
16	Conor Reynolds	Formalizing the Institution for Event-B in the Coq Proof Assistant.	ABZ	2021	DBLP DOI BibTeX RDF
16	Rajeev Goré, Revantha Ramanayake, Ian Shillito	Cut-Elimination for Provability Logic by Terminating Proof-Search: Formalised and Deconstructed Using Coq.	TABLEAUX	2021	DBLP DOI BibTeX RDF
16	Lennard Gäher, Fabian Kunze	Mechanising Complexity Theory: The Cook-Levin Theorem in Coq.	ITP	2021	DBLP DOI BibTeX RDF
16	Dominik Kirst, Marc Hermes	Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq.	ITP	2021	DBLP DOI BibTeX RDF
16	Luís Cruz-Filipe, Fabrizio Montesi, Marco Peressotti	Formalising a Turing-Complete Choreographic Language in Coq.	ITP	2021	DBLP DOI BibTeX RDF
16	Pierre Nigron, Pierre-Évariste Dagand	Reaching for the Star: Tale of a Monad in Coq.	ITP	2021	DBLP DOI BibTeX RDF
16	Véronique Benzaken, Sarah Cohen-Boulakia, Evelyne Contejean, Chantal Keller, Rébecca Zucchini	A Coq formalization of data provenance.	CPP	2021	DBLP DOI BibTeX RDF
16	Dominik Kirst, Felix Rech	The generalised continuum hypothesis implies the axiom of choice in Coq.	CPP	2021	DBLP DOI BibTeX RDF
16	Koundinya Vajjha, Avraham Shinnar, Barry M. Trager, Vasily Pestun, Nathan Fulton	CertRL: formalizing convergence proofs for value and policy iteration in Coq.	CPP	2021	DBLP DOI BibTeX RDF
16	Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters	Extracting smart contracts tested and verified in Coq.	CPP	2021	DBLP DOI BibTeX RDF
16	Pierre-Léo Bégay, Pierre Crégut, Jean-François Monin	Developing and certifying Datalog optimizations in coq/mathcomp.	CPP	2021	DBLP DOI BibTeX RDF
16	Lucien Rakotomalala, Pierre Roux, Marc Boyer	Verifying Min-Plus Computations with Coq.	NFM	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.	ICSE (Companion Volume)	2021	DBLP DOI BibTeX RDF
16	Yannick Forster 0002	Church's Thesis and Related Axioms in Coq's Type Theory.	CSL	2021	DBLP DOI BibTeX RDF
16	Liao Zhang, Lasse Blaauwbroek, Bartosz Piotrowski, Prokop Cerný, Cezary Kaliszyk, Josef Urban	Online Machine Learning Techniques for Coq: A Comparison.	CICM	2021	DBLP DOI BibTeX RDF
16	Fritjof Bornebusch	Coq meets CλaSH: proposing a hardware design synthesis flow that combines proof assistants with functional hardware description languages		2021	RDF
16	Ángel Francisco Zúñiga Chávez	Semántica natural como marco de verificación de compiladores en Coq		2021	RDF
16	Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, Steve Zdancewic	Interaction trees: representing recursive and impure programs in Coq.	Proc. ACM Program. Lang.	2020	DBLP DOI BibTeX RDF
16	Zheng Cheng, Massimo Tisi, Rémi Douence	CoqTL: a Coq DSL for rule-based model transformation.	Softw. Syst. Model.	2020	DBLP DOI BibTeX RDF
16	Zheng Yang 0007, Hang Lei, Weizhong Qian	A Hybrid Formal Verification System in Coq for Ensuring the Reliability and Security of Ethereum-Based Service Smart Contracts.	IEEE Access	2020	DBLP DOI BibTeX RDF
16	Tianyu Sun, Wensheng Yu	A Formal System of Axiomatic Set Theory in Coq.	IEEE Access	2020	DBLP DOI BibTeX RDF
16	Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters	Extracting Smart Contracts Tested and Verified in Coq.	CoRR	2020	DBLP BibTeX RDF
16	Dominique Larchey-Wendling, Yannick Forster 0002	Hilbert's Tenth Problem in Coq.	CoRR	2020	DBLP BibTeX RDF
16	Yannick Forster 0002	Church's thesis and related axioms in Coq's type theory.	CoRR	2020	DBLP BibTeX RDF
16	Koundinya Vajjha, Avraham Shinnar, Vasily Pestun, Barry M. Trager, Nathan Fulton	CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq.	CoRR	2020	DBLP BibTeX RDF
16	Lasse Blaauwbroek, Josef Urban, Herman Geuvers	Tactic Learning and Proving for the Coq Proof Assistant.	CoRR	2020	DBLP BibTeX RDF
16	Wenjun Shi, Qinxiang Cao, Yuxin Deng, Hanru Jiang, Yuan Feng 0001	Symbolic Reasoning about Quantum Circuits in Coq.	CoRR	2020	DBLP BibTeX RDF
16	Lasse Blaauwbroek, Josef Urban, Herman Geuvers	The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq.	CoRR	2020	DBLP BibTeX RDF
16	Boro Sitnikovski	Formalizing line editors in Coq.	CoRR	2020	DBLP BibTeX RDF
16	Dominik Kirst, Dominique Larchey-Wendling	Trakhtenbrot's Theorem in Coq, A Constructive Approach to Finite Model Theory.	CoRR	2020	DBLP BibTeX RDF
16	Boro Sitnikovski, Biljana Stojcevska, Lidija Goracinova-Ilieva, Irena Stojmenovska	PubSub implementation in Haskell with formal verification in Coq.	CoRR	2020	DBLP BibTeX RDF
16	Pengyu Nie 0001, Karl Palmskog, Junyi Jessy Li, Milos Gligoric 0001	Learning to Format Coq Code Using Language Models.	CoRR	2020	DBLP BibTeX RDF
16	Dimitur Nikolaev Krustev	Experience Report: Smuggling a Little Bit of Coq Inside a CAD Development Context (Extended Abstract).	CoRR	2020	DBLP BibTeX RDF
16	Pengyu Nie 0001, Karl Palmskog, Junyi Jessy Li, Milos Gligoric 0001	Deep Generation of Coq Lemma Names Using Elaborated Terms.	CoRR	2020	DBLP BibTeX RDF
16	Burak Ekici, Cezary Kaliszyk	Mac Lane's Comparison Theorem for the Kleisli Construction Formalized in Coq.	Math. Comput. Sci.	2020	DBLP DOI BibTeX RDF
16	Christian Doczkal, Damien Pous	Graph Theory in Coq: Minors, Treewidth, and Isomorphisms.	J. Autom. Reason.	2020	DBLP DOI BibTeX RDF
16	Jiawei Wang, Ming Fu, Lei Qiao, Xinyu Feng 0001	Formalizing SPARCv8 instruction set architecture in Coq.	Sci. Comput. Program.	2020	DBLP DOI BibTeX RDF
16	Lasse Blaauwbroek, Josef Urban, Herman Geuvers	Tactic Learning and Proving for the Coq Proof Assistant.	LPAR	2020	DBLP DOI BibTeX RDF
16	Hao Bu, Meng Sun 0002	Towards Modeling and Verification of the CKB Block Synchronization Protocol in Coq.	ICFEM	2020	DBLP DOI BibTeX RDF
16	Elaine Li, Traian Serbanuta, Denisa Diaconescu, Vlad Zamfir, Grigore Rosu	Formalizing Correct-by-Construction Casper in Coq.	IEEE ICBC	2020	DBLP DOI BibTeX RDF
16	Bruno Bernardo, Raphaël Cauderlier, Guillaume Claret, Arvid Jakobsson, Basile Pesin, Julien Tesson	Making Tezos Smart Contracts More Reliable with Coq.	ISoLA (3)	2020	DBLP DOI BibTeX RDF
16	Matteo Cavada, Andrea Colò, Alberto Momigliano	MutantChick: Type-Preserving Mutation Analysis for Coq.	CILC	2020	DBLP BibTeX RDF
16	Rafael Castro G. Silva, Cristiano D. Vasconcellos, Karina Girardi Roggia	Monadic W in Coq.	SBLP	2020	DBLP DOI BibTeX RDF
16	Cyril Cohen, Kazuhiko Sakaguchi, Enrico Tassi	Hierarchy Builder: Algebraic hierarchies Made Easy in Coq with Elpi (System Description).	FSCD	2020	DBLP DOI BibTeX RDF
16	Zheng Yang 0007, Hang Lei, Weizhong Qian, Zehui Yan, Weiru Zeng	A Resolution for Scalability Problem of Record Datatype Based Formal Memory Models in Coq.	CSAE	2020	DBLP DOI BibTeX RDF
16	Matteo Manighetti, Dale Miller 0001, Alberto Momigliano	Two Applications of Logic Programming to Coq.	TYPES	2020	DBLP DOI BibTeX RDF
16	Dominik Kirst, Dominique Larchey-Wendling	Trakhtenbrot's Theorem in Coq - A Constructive Approach to Finite Model Theory.	IJCAR (2)	2020	DBLP DOI BibTeX RDF
16	Pengyu Nie 0001, Karl Palmskog, Junyi Jessy Li, Milos Gligoric 0001	Deep Generation of Coq Lemma Names Using Elaborated Terms.	IJCAR (2)	2020	DBLP DOI BibTeX RDF
16	Lukasz Czajka 0001	Practical Proof Search for Coq by Type Inhabitation.	IJCAR (2)	2020	DBLP DOI BibTeX RDF
16	Thayonara Alves, Leopoldo Teixeira, Vander Alves, Thiago M. Castro	Porting the Software Product Line Refinement Theory to the Coq Proof Assistant.	SBMF	2020	DBLP DOI BibTeX RDF
16	Danil Annenkov, Jakob Botsch Nielsen, Bas Spitters	ConCert: a smart contract certification framework in Coq.	CPP	2020	DBLP DOI BibTeX RDF
16	Simon Spies, Yannick Forster 0002	Undecidability of higher-order unification formalised in Coq.	CPP	2020	DBLP DOI BibTeX RDF
16	Yannick Forster 0002, Kathrin Stark	Coq à la carte: a practical approach to modular syntax with binders.	CPP	2020	DBLP DOI BibTeX RDF
16	Talia Ringer, Alex Sanchez-Stern, Dan Grossman, Sorin Lerner	REPLica: REPL instrumentation for Coq analysis.	CPP	2020	DBLP DOI BibTeX RDF
16	Yannick Forster 0002, Fabian Kunze, Maxi Wuttke	Verified programming of Turing machines in Coq.	CPP	2020	DBLP DOI BibTeX RDF
16	Christian Doczkal, Damien Pous	Completeness of an axiomatization of graph isomorphism via graph rewriting in Coq.	CPP	2020	DBLP DOI BibTeX RDF
16	Thomas Letan, Yann Régis-Gianas	FreeSpec: specifying, verifying, and executing impure computations in Coq.	CPP	2020	DBLP DOI BibTeX RDF
16	Kush Jain, Karl Palmskog, Ahmet Çelik, Emilio Jesús Gallego Arias, Milos Gligoric 0001	mCoq: mutation analysis for Coq verification projects.	ICSE (Companion Volume)	2020	DBLP DOI BibTeX RDF
16	Samir Ouchani, Khaled Khebbeb, Meriem Hafsi	Towards Enhancing Security and Resilience in CPS: A Coq-Maude based Approach.	AICCSA	2020	DBLP DOI BibTeX RDF
16	Lasse Blaauwbroek, Josef Urban, Herman Geuvers	The Tactician - A Seamless, Interactive Tactic Learner and Prover for Coq.	CICM	2020	DBLP DOI BibTeX RDF
16	Kathrin Stark	Mechanising syntax with binders in Coq.		2020	RDF
16	Matthieu Sozeau, Cyprien Mangin	Equations reloaded: high-level dependently-typed functional programming and proving in Coq.	Proc. ACM Program. Lang.	2019	DBLP DOI BibTeX RDF
16	Zheng Yang 0007, Hang Lei	FEther: An Extensible Definitional Interpreter for Smart-Contract Verifications in Coq.	IEEE Access	2019	DBLP DOI BibTeX RDF
16	Fabio Alessi, Alberto Ciaffaglione, Pietro Di Gianantonio, Furio Honsell, Marina Lenisa, Ivan Scagnetto	LF+ in Coq for "fast and loose" reasoning.	J. Formaliz. Reason.	2019	DBLP DOI BibTeX RDF
16	Jakob Botsch Nielsen, Bas Spitters	Smart Contract Interactions in Coq.	CoRR	2019	DBLP BibTeX RDF
16	Musab A. Alturki, Jing Chen, Victor Luchangco, Brandon M. Moore, Karl Palmskog, Lucas Peña, Grigore Rosu	Towards a Verified Model of the Algorand Consensus Protocol in Coq.	CoRR	2019	DBLP BibTeX RDF
16	Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, Steve Zdancewic	Interaction Trees: Representing Recursive and Impure Programs in Coq (Work In Progress).	CoRR	2019	DBLP BibTeX RDF
16	Florian Steinberg 0001, Laurent Théry, Holger Thies	Quantitative continuity and computable analysis in Coq.	CoRR	2019	DBLP BibTeX RDF
16	Zheng Yang 0007, Hang Lei, Weizong Qian	A Hybrid Formal Verification System in Coq for Ensuring the Reliability and Security of Ethereum-based Service Smart Contracts.	CoRR	2019	DBLP BibTeX RDF
16	Gérard Berry, Lionel Rieg	Towards Coq-verified Esterel Semantics and Compiling.	CoRR	2019	DBLP BibTeX RDF
16	Jonathan Chan, William J. Bowman	Practical Sized Typing for Coq.	CoRR	2019	DBLP BibTeX RDF
16	Yannick Forster 0002, Fabian Kunze	A certifying extraction with time bounds from Coq to call-by-value $λ$-calculus.	CoRR	2019	DBLP BibTeX RDF
16	Danil Annenkov, Bas Spitters	Towards a Smart Contract Verification Framework in Coq.	CoRR	2019	DBLP BibTeX RDF
16	Gustavo Carvalho, Igor Meira	Modelling and testing timed data-flow reactive systems in Coq from controlled natural-language requirements.	CoRR	2019	DBLP BibTeX RDF
16	Burak Ekici, Arjun Viswanathan, Yoni Zohar, Clark W. Barrett, Cesare Tinelli	Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract).	PxTP	2019	DBLP DOI BibTeX RDF
16	Andrei Arusoaie	A Formal Semantics of Findel in Coq (Short Paper).	CoRR	2019	DBLP BibTeX RDF
16	Bruno Bernardo, Raphaël Cauderlier, Zhenlei Hu, Basile Pesin, Julien Tesson	Mi-Cho-Coq, a framework for certifying Tezos Smart Contracts.	CoRR	2019	DBLP BibTeX RDF
16	Fabio Alessi, Alberto Ciaffaglione, Pietro Di Gianantonio, Furio Honsell, Marina Lenisa	A Definitional Implementation of the Lax Logical Framework LLFP in Coq, for Supporting Fast and Loose Reasoning.	LFMTP@LICS	2019	DBLP DOI BibTeX RDF
16	Pierre Boutry, Charly Gries, Julien Narboux, Pascal Schreck	Parallel Postulates and Continuity Axioms: A Mechanized Study in Intuitionistic Logic Using Coq.	J. Autom. Reason.	2019	DBLP DOI BibTeX RDF
16	Yannick Forster 0002, Gert Smolka	Call-by-Value Lambda Calculus as a Model of Computation in Coq.	J. Autom. Reason.	2019	DBLP DOI BibTeX RDF
16	Xiyue Zhang, Weijiang Hong, Yi Li 0010, Meng Sun 0002	Reasoning about connectors using Coq and Z3.	Sci. Comput. Program.	2019	DBLP DOI BibTeX RDF
16	Zhenwei Ma, Gang Chen	基于Coq记录的矩阵形式化方法 (Matrix Formalization Based on Coq Record).	计算机科学	2019	DBLP DOI BibTeX RDF
16	Sergey Bozhko, Leyla Khatbullina, Semyon V. Grigorev	Bar-Hillel Theorem Mechanization in Coq.	WoLLIC	2019	DBLP DOI BibTeX RDF
16	Nitin Bhatia, Meenakshi D'Souza, Sujit Kumar Chakrabarti	Formalizing GPU Instruction Set Architecture in Coq.	ISEC	2019	DBLP DOI BibTeX RDF
16	Salwa Souaf, Frédéric Loulergue	A First Step in the Translation of Alloy to Coq.	ICFEM	2019	DBLP DOI BibTeX RDF
16	Jolan Philippe, Frédéric Loulergue	Parallel programming with Coq: map and reduce skeletons on trees.	SAC	2019	DBLP DOI BibTeX RDF
16	Benjamin Ferrell, Jun Duan, Kevin W. Hamlen	CUDA au Coq: A Framework for Machine-validating GPU Assembly Programs.	DATE	2019	DBLP DOI BibTeX RDF
16	Bruno Bernardo, Raphaël Cauderlier, Zhenlei Hu, Basile Pesin, Julien Tesson	Mi-Cho-Coq, a Framework for Certifying Tezos Smart Contracts.	FM Workshops (1)	2019	DBLP DOI BibTeX RDF
16	Jakob Botsch Nielsen, Bas Spitters	Smart Contract Interactions in Coq.	FM Workshops (1)	2019	DBLP DOI BibTeX RDF
16	Musab A. Alturki, Jing Chen, Victor Luchangco, Brandon M. Moore, Karl Palmskog, Lucas Peña, Grigore Rosu	Towards a Verified Model of the Algorand Consensus Protocol in Coq.	FM Workshops (1)	2019	DBLP DOI BibTeX RDF
16	Siran Lei, Mengqi Cheng, Jianguo Jiang	Tactics for Proving Separation Logic Assertion in Coq Proof Assistant.	ICVISP	2019	DBLP DOI BibTeX RDF
16	Yuxin Deng, Jean-François Monin	Formalisation of Probabilistic Testing Semantics in Coq.	The Art of Modelling Computational Systems	2019	DBLP DOI BibTeX RDF
16	Kosuke Murata, Kento Emoto	Recursion Schemes in Coq.	APLAS	2019	DBLP DOI BibTeX RDF
16	Alexander Bagnall, Gordon Stewart 0001	Certifying the True Error: Machine Learning in Coq with Verified Generalization Guarantees.	AAAI	2019	DBLP DOI BibTeX RDF
16	Florian Faissole, George A. Constantinides, David B. Thomas	Formalizing Loop-Carried Dependencies in Coq for High-Level Synthesis.	FCCM	2019	DBLP DOI BibTeX RDF
16	Raul Fervari, Francisco Trucco, Beta Ziliani	Mechanizing Bisimulation Theorems for Relation-Changing Logics in Coq.	DaLí	2019	DBLP DOI BibTeX RDF