Search results for "Coq"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
69	Milad Niqui	Coalgebraic Reasoning in Coq: Bisimulation and the lambda-Coiteration Scheme.	TYPES	2008	DBLP DOI BibTeX RDF	Coiteration, Bisimulation, Coalgebra, Coq, Coinduction
69	Xingyuan Zhang, Malcolm Munro, Mark Harman, Lin Hu 0005	Weakest Precondition for General Recursive Programs Formalized in Coq.	TPHOLs	2002	DBLP DOI BibTeX RDF	Formal Verification, Operational Semantics, Weakest Precondition, Coq
69	Amy P. Felty	Two-Level Meta-reasoning in Coq.	TPHOLs	2002	DBLP DOI BibTeX RDF
69	Kumar Neeraj Verma, Jean Goubault-Larrecq, Sanjiva Prasad, S. Arun-Kumar	Reflecting BDDs in Coq.	ASIAN	2000	DBLP DOI BibTeX RDF
68	César Domínguez 0001	Formalizing in Coq Hidden Algebras to Specify Symbolic Computation Systems.	AISC/MKM/Calculemus	2008	DBLP DOI BibTeX RDF	hidden algebras, symbolic computation, Coq proof assistant
63	Matthieu Sozeau, Simon Boulier, Yannick Forster 0002, Nicolas Tabareau, Théo Winterhalter	Coq Coq correct! verification of type checking and erasure for Coq, in Coq.	Proc. ACM Program. Lang.	2020	DBLP DOI BibTeX RDF
59	Nicolas Magaud, Julien Narboux, Pascal Schreck	Formalizing Desargues' theorem in Coq using ranks.	SAC	2009	DBLP DOI BibTeX RDF	Desargues, rank, formalization, projective geometry, Coq
58	Matthieu Sozeau	Subset Coercions in Coq.	TYPES	2006	DBLP DOI BibTeX RDF
58	Pierre Letouzey	A New Extraction for Coq.	TYPES	2002	DBLP DOI BibTeX RDF
58	David Delahaye	A Tactic Language for the System Coq.	LPAR	2000	DBLP DOI BibTeX RDF
58	Mickaël Kerboeuf, David Nowak, Jean-Pierre Talpin	Specification and Verification of a Steam-Boiler with Signal-Coq.	TPHOLs	2000	DBLP DOI BibTeX RDF	the steam-boiler problem, theorem proving, synchronous programming
53	Venanzio Capretta, Bernard Stepien, Amy P. Felty, Stan Matwin	Formal correctness of conflict detection for firewalls.	FMSE	2007	DBLP DOI BibTeX RDF	firewall, coq
48	Tuan Minh Pham	Similar triangles and orientation in plane elementary geometry for Coq-based proofs.	SAC	2010	DBLP DOI BibTeX RDF	similar triangles, orientation, formalization, Coq, geometric theorem proving
48	Sidi Ould Biha	Finite Groups Representation Theory with Coq.	Calculemus/MKM	2009	DBLP DOI BibTeX RDF	Maschke’s theorem, SSReflect, linear algebra, Coq, Representation theory
48	Wendy Verbruggen, Edsko de Vries, Arthur Hughes	Polytypic programming in COQ.	ICFP-WGP	2008	DBLP DOI BibTeX RDF	kind-indexed types, theorem proving, generic programming, formalization, coq, polytypic programming
48	Boutheina Chetali, Barbara Heyd	Formal Verification of Concurrent Programs in LP and in COQ: A Comparative Analysis.	TPHOLs	1997	DBLP DOI BibTeX RDF	theorem prover methodology, Larch Prover, Computer Checked Proof, Formal Verification, Unity, Coq
47	Hai Wan, Gang Chen 0004, Xiaoyu Song, Ming Gu 0001	Formalization and Verification of PLC Timers in Coq.	COMPSAC (1)	2009	DBLP DOI BibTeX RDF
47	Stéphane Lescuyer, Sylvain Conchon	Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme.	FroCoS	2009	DBLP DOI BibTeX RDF
47	Pierre Letouzey	Extraction in Coq: An Overview.	CiE	2008	DBLP DOI BibTeX RDF
47	Jacek Chrzaszcz, Daria Walukiewicz-Chrzaszcz	Towards Rewriting in Coq.	Rewriting, Computation and Proof	2007	DBLP DOI BibTeX RDF
47	Venanzio Capretta, Amy P. Felty	Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq.	TYPES	2006	DBLP DOI BibTeX RDF
47	Luís Cruz-Filipe, Herman Geuvers, Freek Wiedijk	C-CoRN, the Constructive Coq Repository at Nijmegen.	MKM	2004	DBLP DOI BibTeX RDF
47	Nicolas Magaud	Changing Data Representation within the Coq System.	TPHOLs	2003	DBLP DOI BibTeX RDF
47	Jacek Chrzaszcz	Implementing Modules in the Coq System.	TPHOLs	2003	DBLP DOI BibTeX RDF
47	Reynald Affeldt, Naoki Kobayashi 0001	Formalization and Verification of a Mail Server in Coq.	ISSS	2002	DBLP DOI BibTeX RDF
47	Jean-François Dufourd	An Intuitionistic Proof of a Discrete Form of the Jordan Curve Theorem Formalized in Coq with Combinatorial Hypermaps.	J. Autom. Reason.	2009	DBLP DOI BibTeX RDF	Computer-aided proofs, Coq system, Combinatorial hypermaps, Discrete Jordan Curve Theorem, Formal specifications, Computational topology, Planar subdivisions
43	Jay A. McCarthy, Shriram Krishnamurthi	Minimal backups of cryptographic protocol runs.	FMSE	2008	DBLP DOI BibTeX RDF	cppl, cryptographic protocols, coq, strand spaces
43	Brian E. Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack, Stephanie Weirich	Engineering formal metatheory.	POPL	2008	DBLP DOI BibTeX RDF	locally nameless, binding, coq
43	Benjamin Grégoire, Xavier Leroy	A compiled implementation of strong reduction.	ICFP	2002	DBLP DOI BibTeX RDF	beta-equivalence, calculus of constructions, normalization by evaluation, strong reduction, virtual machine, abstract machine, Coq
42	J. Gregory Malecha, Greg Morrisett, Avraham Shinnar, Ryan Wisnesky	Toward a verified relational database management system.	POPL	2010	DBLP DOI BibTeX RDF	relational model, dependent types, separation logic, b+ tree
42	Evelyne Contejean, Pierre Corbineau	Reflecting Proofs in First-Order Logic with Equality.	CADE	2005	DBLP DOI BibTeX RDF
37	Sylvie Boldo, Jean-Christophe Filliâtre, Guillaume Melquiond	Combining Coq and Gappa for Certifying Floating-Point Programs.	Calculemus/MKM	2009	DBLP DOI BibTeX RDF
37	Florian Kammüller	Formalizing non-interference for a simple bytecode language in Coq.	Formal Aspects Comput.	2008	DBLP DOI BibTeX RDF	Formal methods for security, Programming language analysis, Interactive theorem proving, Modular specification
37	Greg Morrisett	Programming with Effects in Coq.	MPC	2008	DBLP DOI BibTeX RDF
37	Russell O'Connor	Essential Incompleteness of Arithmetic Verified by Coq.	TPHOLs	2005	DBLP DOI BibTeX RDF
37	Lionel Elie Mamane	Surreal Numbers in Coq.	TYPES	2004	DBLP DOI BibTeX RDF
37	Nicolas Oury	Observational Equivalence and Program Extraction in the Coq Proof Assistant.	TLCA	2003	DBLP DOI BibTeX RDF
37	Jacek Chrzaszcz	Modules in Coq Are and Will Be Correct.	TYPES	2003	DBLP DOI BibTeX RDF
37	Milad Niqui, Yves Bertot	QArith: Coq Formalisation of Lazy Rational Arithmetic.	TYPES	2003	DBLP DOI BibTeX RDF
37	Laurent Chicli, Loic Pottier, Carlos Simpson	Mathematical Quotients and Quotient Types in Coq.	TYPES	2002	DBLP DOI BibTeX RDF
37	Venanzio Capretta	Certifying the Fast Fourier Transform with Coq.	TPHOLs	2001	DBLP DOI BibTeX RDF
37	Christine Paulin-Mohring	Modelisation of Timed Automata in Coq.	TACS	2001	DBLP DOI BibTeX RDF
37	José Luis Freire, José E. Freire Brañas, Antonio Blanco Ferro, Juan J. Sánchez Penas	Fusion in Coq.	EUROCAST	2001	DBLP DOI BibTeX RDF
37	Ewen Denney	A Prototype Proof Translator from HOL to Coq.	TPHOLs	2000	DBLP DOI BibTeX RDF
37	Herman Geuvers, Milad Niqui	Constructive Reals in Coq: Axioms and Categoricity.	TYPES	2000	DBLP DOI BibTeX RDF
37	Solange Coupet-Grimal, Line Jakubiec	Hardware Verification Using Co-induction in COQ.	TPHOLs	1999	DBLP DOI BibTeX RDF
37	David Delahaye	Information Retrieval in a Coq Proof Library Using Type Isomorphisms.	TYPES	1999	DBLP DOI BibTeX RDF
37	Christoph Sprenger 0001	A Verified Model Checker for the Modal µ-calculus in Coq.	TACAS	1998	DBLP DOI BibTeX RDF
36	Laurence Rideau, Bernard P. Serpette, Xavier Leroy	Tilting at Windmills with Coq: Formal Verification of a Compilation Algorithm for Parallel Moves.	J. Autom. Reason.	2008	DBLP DOI BibTeX RDF	Parallel move, Parallel assignment, The Coq proof assistant, Compilation, Compiler correctness
34	Ina Ganguli, Marieke Huysentruyt, Chloé Le Coq	How Do Nascent Social Entrepreneurs Respond to Rewards? A Field Experiment on Motivations in a Grant Competition.	Manag. Sci.	2021	DBLP DOI BibTeX RDF
34	Basem Aqlan, Mohamed Himdi, Hamsakutty Vettikalladi, Laurent Le Coq	A Circularly Polarized Sub-Terahertz Antenna With Low-Profile and High-Gain for 6G Wireless Communication Systems.	IEEE Access	2021	DBLP DOI BibTeX RDF
34	Laurent Le Coq, Nicolas Mézières, Paul Leroy, Benjamin Fuchs	Some Contributions for Antenna 3D Far Field Characterization at Terahertz.	Sensors	2021	DBLP DOI BibTeX RDF
34	Rosine Coq Germanicus, Florent Lallemand, Nicolas Normand, Catherine Bunel, Ulrike Lüders	Integrated 3D-Capacitors for Implantable Bradycardia Pacemakers: Dielectric Integrity and Local Electrical Characterizations using AFM.	BIODEVICES	2021	DBLP DOI BibTeX RDF
34	Basem Aqlan, Mohamed Himdi, Laurent Le Coq, Hamsakutty Vettikalladi	Sub-THz Circularly Polarized Horn Antenna Using Wire Electrical Discharge Machining for 6G Wireless Communications.	IEEE Access	2020	DBLP DOI BibTeX RDF
34	Edward C. McCain, Pascal Bastien, Brenton F. Belmar, Barin Bhattacharya, Kennedy K. Cheruiyot, Marc Coq, Ronald Dartey, Kavitha Deekaram, Kharavel Ghadai, Lucas D. LaLima, Jeffrey Nettey, Adeoye O. Owolabi, Kyle Phillips, Tyler M. Shiling, Dominic T. Schroeder, Craig M. Slegel, Bradley Steen, Daniel Alexander Thorne, Emily Venuto, Jeffrey D. Willoughby, Daniela Yaniv, Nicholas Ziemis	IBM Z development transformation.	IBM J. Res. Dev.	2020	DBLP DOI BibTeX RDF
34	Cyril Tissot, Etienne Neethling, Mathias Rouan, Gérard Barbeau, Hervé Quénol, Céline Le Coq	Modeling Environmental Impacts on Viticultural Ecosystems: A First Case Study in a Regulated Wine Producing Area.	Int. J. Agric. Environ. Inf. Syst.	2017	DBLP DOI BibTeX RDF
34	Pascal Masselin, Eugene Bychkov, David Le Coq	New strategy for direct laser writing of low loss waveguide.	ICTON	2017	DBLP DOI BibTeX RDF
34	Marco Donald Migliore, Laurent Le Coq, Benjamin Fuchs	An investigation on an interference filtering technique for array diagnosis using sparsity.	M&N	2017	DBLP DOI BibTeX RDF
34	David Le Coq, O. Caulier, Eugene Bychkov, Johann Troles, Pascal Masselin	Inscription of infrared waveguides in chalcogenide glasses by femtosecond laser.	ICTON	2015	DBLP DOI BibTeX RDF
34	Jingyue Li, Torbjørn Skramstad, Thierry Coq	Interface Information Management Tools for the Maritime and Oil and Gas Industry.	COMPSAC Workshops	2015	DBLP DOI BibTeX RDF
34	Mikhail Gurov, J. J. McFerran, Bartlomiej Nagorny, R. Tyumenev, Z. Xu, Y. Le Coq, Rodolphe Le Targat, Pierre Lemonde, Jérôme Lodewyck, S. Bize	Optical Lattice Clocks as Candidates for a Possible Redefinition of the SI Second.	IEEE Trans. Instrum. Meas.	2013	DBLP DOI BibTeX RDF
34	Alastair I. Matheson, Janet G. Baseman, Stephen H. Wagner, Gabrielle E. O'Malley, Nancy H. Puttkammer, Emmlyne Emmanuel, Garry Zamor, Rikerdy Frédéric, Nancy R. Coq, William B. Lober	Implementation and expansion of an electronic medical record for HIV care and treatment in Haiti: An assessment of system use and the impact of large-scale disruptions.	Int. J. Medical Informatics	2012	DBLP DOI BibTeX RDF
34	Davide Falessi, Mehrdad Sabetzadeh, Lionel C. Briand, Emanuele Turella, Thierry Coq, Rajwinder Kaur Panesar-Walawege	Planning for Safety Standards Compliance: A Model-Based Tool-Supported Approach.	IEEE Softw.	2012	DBLP DOI BibTeX RDF
34	Shiva Nejati, Mehrdad Sabetzadeh, Davide Falessi, Lionel C. Briand, Thierry Coq	A SysML-based approach to traceability management and design slicing in support of safety certification: Framework, tool support, and case studies.	Inf. Softw. Technol.	2012	DBLP DOI BibTeX RDF
34	Cédric Le Coq, Adellah Tougui, Marie-Pascale Stempin, Laurent Barreau	Optimization for simulation of WL-CSP subjected to drop-test with plasticity behavior.	Microelectron. Reliab.	2011	DBLP DOI BibTeX RDF
34	Arnold James D'Souza, Ravpreet Singh, J. Raja Prabhu, Gajendranath Chowdary, Ankit Seedher, Shyam Somayajula, Nageswara Rao Nalam, Lionel Cimaz, Stephane Le Coq, Praveen Kallam, Siddharth Sundar, Shanfeng Cheng, Sanjay Tumati, Wenchang Huang	A fully integrated power-management solution for a 65nm CMOS cellular handset chip.	ISSCC	2011	DBLP DOI BibTeX RDF
34	Thierry Coq, Jean-Pierre Rosen	The SQALE Quality and Analysis Models for Assessing the Quality of Ada Source Code.	Ada-Europe	2011	DBLP DOI BibTeX RDF
34	Cédric Le Coq, Adellah Tougui, Marie-Pascale Stempin, Laurent Barreau	Experimental study of WL-CSP reliability subjected to a four-point bend-test.	Microelectron. Reliab.	2010	DBLP DOI BibTeX RDF
34	Rajwinder Kaur Panesar-Walawege, Mehrdad Sabetzadeh, Lionel C. Briand, Thierry Coq	Characterizing the Chain of Evidence for Software Safety Cases: A Conceptual Model Based on the IEC 61508 Standard.	ICST	2010	DBLP DOI BibTeX RDF
34	Guilhem Coq, X. Li, Olivier Alata, Yannis Pousset, Christian Olivier	Law recognition via histogram-based estimation.	ICASSP	2009	DBLP DOI BibTeX RDF
34	Guilhem Coq	Utilisation d'approches probabilistes basées sur les critères entropiques pour la recherche d'information sur supports multimédia.		2008	RDF
34	Guilhem Coq, Olivier Alata, Marc Arnaudon, Christian Olivier	Information Criteria and Arithmetic Codings : An Illustration on Raw Images	CoRR	2007	DBLP BibTeX RDF
34	François Alouges, Gérard Le Coq, Emmanuel Lorin	Two-Dimensional Extension of the Reservoir Technique for Some Linear Advection Systems.	J. Sci. Comput.	2007	DBLP DOI BibTeX RDF	Multidimensional convection, finite volume schemes, reservoirs, numerical diffusion
34	Guilhem Coq, Christian Olivier, Olivier Alata, Marc Arnaudon	Information criteria and arithmetic codings : An illustration on raw images.	EUSIPCO	2007	DBLP BibTeX RDF
34	Antoine Courteille, Philippe Allot, Jean-Pierre Tarditi, Jean-Louis Ermine, Marc Le Coq	Ingénierie des connaissances et innovation - Application dans le domaine automobile.	EGC	2002	DBLP BibTeX RDF
32	François Garillot, Georges Gonthier, Assia Mahboubi, Laurence Rideau	Packaging Mathematical Structures.	TPHOLs	2009	DBLP DOI BibTeX RDF	Formalization of Algebra, Coercive subtyping, SSReflect, Type inference, Coq
32	Stéphane Le Roux 0001	Acyclic Preferences and Existence of Sequential Nash Equilibria: A Formal and Constructive Equivalence.	TPHOLs	2009	DBLP DOI BibTeX RDF	sequential game theory, effective generalisation, abstraction, induction, Coq
32	Jean Goubault-Larrecq	Towards Producing Formally Checkable Security Proofs, Automatically.	CSF	2008	DBLP DOI BibTeX RDF	Dolev-Yao model, h1, security, model-checking, first-order logic, tree automata, proofs, Coq, Paradox
32	Yves Bertot, Ekaterina Komendantskaya	Using Structural Recursion for Corecursion.	TYPES	2008	DBLP DOI BibTeX RDF	Constructive Type Theory, Structural Recursion, Coinductive types, Guarded Corecursion, Coq
32	Julien Narboux	A Graphical User Interface for Formal Proofs in Geometry.	J. Autom. Reason.	2007	DBLP DOI BibTeX RDF	Interface, Geometry, Automated theorem proving, Theorem prover, Proof assistant, Coq, Dynamic geometry
32	Felicidad Aguado, José Luis Doncel, José María Molinelli, Gilberto Pérez 0001, Concepción Vidal, Ana María Vieites	Certified Genetic Algorithms: Crossover Operators for Permutations.	EUROCAST	2007	DBLP DOI BibTeX RDF	Calculus of Inductive Constructions, Genetic Algorithm, Specification, Theorem Proving, Crossover, Coq
32	Marc Mehdi Ayadi, Dominique Bolignano	Verification of Cryptographic Protocols: An Experiment.	FME	1997	DBLP DOI BibTeX RDF	security, formal methods, cryptographic protocols, Coq
32	Rébecca Zucchini	Bibliothèque certifiée en Coq pour la provenance des données. (A Coq certified library for data provenance).		2023	RDF
32	Shenghao Yuan	Verified programming and secure integration of operating system libraries in Coq. (Programmation vérifiée et intégration sécurisée de bibliothèques de systèmes d'exploitation dans Coq).		2023	RDF
32	Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters	Extracting functional programs from Coq, in Coq.	J. Funct. Program.	2022	DBLP DOI BibTeX RDF
32	Mario Frank 0002	The Coq Proof Script Visualiser (coq-psv).	CoRR	2021	DBLP BibTeX RDF
32	Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters	Extracting functional programs from Coq, in Coq.	CoRR	2021	DBLP BibTeX RDF
32	Sylvain Boulmé	Formally Verified Defensive Programming (efficient Coq-verified computations from untrusted ML oracles). (Programmation défensive formellement vérifiée (calculs efficaces et vérifiés en Coq, à partir d'oracles OCaml potentiellement non fiables)).		2021	RDF
32	Diane Gallois-Wong	Formalisation en Coq des algorithmes de filtre numérique calculés en précision finie. (Coq formalization of digital filter algorithms computed using finite precision arithmetic).		2021	RDF
32	Pierre-Léo Bégay	Developing and certifying in Coq/MathComp of Datalog optimizations for network verification. (Développement et certification en Coq/MathComp d'optimisations Datalog pour la vérification réseau).		2021	RDF
32	Mohammed Houssem Eddine Hachmaoui	Traduction mécanisée et certifiée en Coq d'une algèbre relationnelle étendue pour SQL vers une algèbre imbriquée. (A Coq certified translation from an extension of relational algebra for SQL to a nested algebra).		2020	RDF
32	Boubacar Demba Sall	Programmation impérative par raffinements avec l'assistant de preuve Coq. (Imperative programming by refinement in the Coq proof assistant).		2020	RDF
32	Enrico Tassi	Deriving Proved Equality Tests in Coq-Elpi: Stronger Induction Principles for Containers in Coq.	ITP	2019	DBLP DOI BibTeX RDF
32	David Braun	Approche combinatoire pour l'automatisation en Coq des preuves formelles en géométrie d'incidence projective. (Combinatorial approach for the automation in Coq of formal proofs in incidence projective geometry).		2019	RDF
32	Guillaume Claret	Program in Coq. (Programmer en Coq).		2018	RDF
32	Jean-Pierre Jouannaud, Pierre-Yves Strub	Coq without Type Casts: A Complete Proof of Coq Modulo Theory.	LPAR	2017	DBLP DOI BibTeX RDF
32	Stefania-Gabriela Dumbrava	Formalisation en Coq de Bases de Données Relationnelles et Déductives -et Mécanisation de Datalog. (A Coq Formalization of Relational and Deductive Databases -and a Mechanizations of Datalog).		2016	RDF
32	Catherine Lelay	Repenser la bibliothèque réelle de Coq : vers une formalisation de l'analyse classique mieux adaptée. (Reinventing Coq's Reals library : toward a more suitable formalization of classical analysis).		2015	RDF
32	Jaime Gaspar	Short Introduction by Example to Coq and Formalising ZF ⊆ ZFε in Coq.	CICM Workshops	2014	DBLP BibTeX RDF
32	Pierre Boutillier	De nouveaux outils pour calculer avec des inductifs en Coq. (New tool to compute with inductive in Coq).		2014	RDF