|
|
Venues (Conferences, Journals, ...)
|
|
GrowBag graphs for keyword ? (Num. hits/coverage)
Group by:
The graphs summarize 294 occurrences of 173 keywords
|
|
|
Results
Found 973 publication records. Showing 959 according to the selection in the facets
Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
69 | Milad Niqui |
Coalgebraic Reasoning in Coq: Bisimulation and the lambda-Coiteration Scheme. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, International Conference, TYPES 2008, Torino, Italy, March 26-29, 2008, Revised Selected Papers, pp. 272-288, 2008, Springer, 978-3-642-02443-6. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002, Proceedings, pp. 332-348, 2002, Springer, 3-540-44039-9. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
Formal Verification, Operational Semantics, Weakest Precondition, Coq |
69 | Amy P. Felty |
Two-Level Meta-reasoning in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002, Proceedings, pp. 198-213, 2002, Springer, 3-540-44039-9. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
69 | Kumar Neeraj Verma, Jean Goubault-Larrecq, Sanjiva Prasad, S. Arun-Kumar |
Reflecting BDDs in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ASIAN ![In: Advances in Computing Science - ASIAN 2000, 6th Asian Computing Science Conference, Penang, Malaysia, November 25-27, 2000, Proceedings, pp. 162-181, 2000, Springer, 3-540-41428-2. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
68 | César Domínguez 0001 |
Formalizing in Coq Hidden Algebras to Specify Symbolic Computation Systems. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AISC/MKM/Calculemus ![In: Intelligent Computer Mathematics, 9th International Conference, AISC 2008, 15th Symposium, Calculemus 2008, 7th International Conference, MKM 2008, Birmingham, UK, July 28 - August 1, 2008. Proceedings, pp. 270-284, 2008, Springer, 978-3-540-85109-7. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Proc. ACM Program. Lang. ![In: Proc. ACM Program. Lang. 4(POPL), pp. 8:1-8:28, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
59 | Nicolas Magaud, Julien Narboux, Pascal Schreck |
Formalizing Desargues' theorem in Coq using ranks. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SAC ![In: Proceedings of the 2009 ACM Symposium on Applied Computing (SAC), Honolulu, Hawaii, USA, March 9-12, 2009, pp. 1110-1115, 2009, ACM, 978-1-60558-166-8. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
Desargues, rank, formalization, projective geometry, Coq |
58 | Matthieu Sozeau |
Subset Coercions in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers, pp. 237-252, 2006, Springer, 978-3-540-74463-4. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
58 | Pierre Letouzey |
A New Extraction for Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, Second International Workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002, Selected Papers, pp. 200-219, 2002, Springer, 3-540-14031-X. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
58 | David Delahaye |
A Tactic Language for the System Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LPAR ![In: Logic for Programming and Automated Reasoning, 7th International Conference, LPAR 2000, Reunion Island, France, November 11-12, 2000, Proceedings, pp. 85-95, 2000, Springer. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
58 | Mickaël Kerboeuf, David Nowak, Jean-Pierre Talpin |
Specification and Verification of a Steam-Boiler with Signal-Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Portland, Oregon, USA, August 14-18, 2000, Proceedings, pp. 356-371, 2000, Springer, 3-540-67863-8. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FMSE ![In: Proceedings of the 2007 ACM workshop on Formal methods in security engineering, FMSE 2007, Fairfax, VA, USA, November 2, 2007, pp. 22-30, 2007, ACM, 978-1-59593-887-9. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
firewall, coq |
48 | Tuan Minh Pham |
Similar triangles and orientation in plane elementary geometry for Coq-based proofs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SAC ![In: Proceedings of the 2010 ACM Symposium on Applied Computing (SAC), Sierre, Switzerland, March 22-26, 2010, pp. 1268-1269, 2010, ACM, 978-1-60558-639-7. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
similar triangles, orientation, formalization, Coq, geometric theorem proving |
48 | Sidi Ould Biha |
Finite Groups Representation Theory with Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Calculemus/MKM ![In: Intelligent Computer Mathematics, 16th Symposium, Calculemus 2009, 8th International Conference, MKM 2009, Held as Part of CICM 2009, Grand Bend, Canada, July 6-12, 2009. Proceedings, pp. 438-452, 2009, Springer, 978-3-642-02613-3. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICFP-WGP ![In: Proceedings of the ACM SIGPLAN Workshop on Generic Programming, WGP 2008, Victoria, BC, Canada, September 20, 2008, pp. 49-60, 2008, ACM, 978-1-60558-060-9. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 10th International Conference, TPHOLs'97, Murray Hill, NJ, USA, August 19-22, 1997, Proceedings, pp. 69-85, 1997, Springer, 3-540-63379-0. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
COMPSAC (1) ![In: Proceedings of the 33rd Annual IEEE International Computer Software and Applications Conference, COMPSAC 2009, Seattle, Washington, USA, July 20-24, 2009. Volume 1, pp. 315-323, 2009, IEEE Computer Society, 978-0-7695-3726-9. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
47 | Stéphane Lescuyer, Sylvain Conchon |
Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FroCoS ![In: Frontiers of Combining Systems, 7th International Symposium, FroCoS 2009, Trento, Italy, September 16-18, 2009. Proceedings, pp. 287-303, 2009, Springer, 978-3-642-04221-8. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
47 | Pierre Letouzey |
Extraction in Coq: An Overview. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CiE ![In: Logic and Theory of Algorithms, 4th Conference on Computability in Europe, CiE 2008, Athens, Greece, June 15-20, 2008, Proceedings, pp. 359-369, 2008, Springer, 978-3-540-69405-2. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
47 | Jacek Chrzaszcz, Daria Walukiewicz-Chrzaszcz |
Towards Rewriting in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Rewriting, Computation and Proof ![In: Rewriting, Computation and Proof, Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of His 60th Birthday, pp. 113-131, 2007, Springer, 978-3-540-73146-7. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
47 | Venanzio Capretta, Amy P. Felty |
Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers, pp. 63-77, 2006, Springer, 978-3-540-74463-4. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
47 | Luís Cruz-Filipe, Herman Geuvers, Freek Wiedijk |
C-CoRN, the Constructive Coq Repository at Nijmegen. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MKM ![In: Mathematical Knowledge Management, Third International Conference, MKM 2004, Bialowieza, Poland, September 19-21, 2004, Proceedings, pp. 88-103, 2004, Springer, 3-540-23029-7. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
47 | Nicolas Magaud |
Changing Data Representation within the Coq System. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 16th International Conference, TPHOLs 2003, Rom, Italy, September 8-12, 2003, Proceedings, pp. 87-102, 2003, Springer, 3-540-40664-6. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
47 | Jacek Chrzaszcz |
Implementing Modules in the Coq System. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 16th International Conference, TPHOLs 2003, Rom, Italy, September 8-12, 2003, Proceedings, pp. 270-286, 2003, Springer, 3-540-40664-6. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
47 | Reynald Affeldt, Naoki Kobayashi 0001 |
Formalization and Verification of a Mail Server in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISSS ![In: Software Security -- Theories and Systems, Mext-NSF-JSPS International Symposium, ISSS 2002, Tokyo, Japan, November 8-10, 2002, Revised Papers, pp. 217-233, 2002, Springer, 3-540-00708-3. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 43(1), pp. 19-51, 2009. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FMSE ![In: Proceedings of the 6th ACM Workshop on Formal Methods in Security Engineering, FMSE 2008, Alexandria, VA, USA, October 27, 2008, pp. 11-20, 2008, ACM, 978-1-60558-288-7. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
POPL ![In: Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008, pp. 3-15, 2008, ACM, 978-1-59593-689-9. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
locally nameless, binding, coq |
43 | Benjamin Grégoire, Xavier Leroy |
A compiled implementation of strong reduction. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICFP ![In: Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP '02), Pittsburgh, Pennsylvania, USA, October 4-6, 2002., pp. 235-246, 2002, ACM, 1-58113-487-8. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
POPL ![In: Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010, pp. 237-248, 2010, ACM, 978-1-60558-479-9. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-20, 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings, pp. 7-22, 2005, Springer, 3-540-28005-7. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
37 | Sylvie Boldo, Jean-Christophe Filliâtre, Guillaume Melquiond |
Combining Coq and Gappa for Certifying Floating-Point Programs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Calculemus/MKM ![In: Intelligent Computer Mathematics, 16th Symposium, Calculemus 2009, 8th International Conference, MKM 2009, Held as Part of CICM 2009, Grand Bend, Canada, July 6-12, 2009. Proceedings, pp. 59-74, 2009, Springer, 978-3-642-02613-3. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
37 | Florian Kammüller |
Formalizing non-interference for a simple bytecode language in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Aspects Comput. ![In: Formal Aspects Comput. 20(3), pp. 259-275, 2008. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MPC ![In: Mathematics of Program Construction, 9th International Conference, MPC 2008, Marseille, France, July 15-18, 2008. Proceedings, pp. 28, 2008, Springer, 978-3-540-70593-2. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
37 | Russell O'Connor |
Essential Incompleteness of Arithmetic Verified by Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings, pp. 245-260, 2005, Springer, 3-540-28372-2. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
37 | Lionel Elie Mamane |
Surreal Numbers in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers, pp. 170-185, 2004, Springer, 3-540-31428-8. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
37 | Nicolas Oury |
Observational Equivalence and Program Extraction in the Coq Proof Assistant. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TLCA ![In: Typed Lambda Calculi and Applications, 6th International Conference, TLCA 2003, Valencia, Spain, June 10-12, 2003, Proceedings., pp. 271-285, 2003, Springer, 3-540-40332-9. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
37 | Jacek Chrzaszcz |
Modules in Coq Are and Will Be Correct. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers, pp. 130-146, 2003, Springer, 3-540-22164-6. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
37 | Milad Niqui, Yves Bertot |
QArith: Coq Formalisation of Lazy Rational Arithmetic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers, pp. 309-323, 2003, Springer, 3-540-22164-6. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
37 | Laurent Chicli, Loic Pottier, Carlos Simpson |
Mathematical Quotients and Quotient Types in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, Second International Workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002, Selected Papers, pp. 95-107, 2002, Springer, 3-540-14031-X. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
37 | Venanzio Capretta |
Certifying the Fast Fourier Transform with Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001, Edinburgh, Scotland, UK, September 3-6, 2001, Proceedings, pp. 154-168, 2001, Springer, 3-540-42525-X. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
37 | Christine Paulin-Mohring |
Modelisation of Timed Automata in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TACS ![In: Theoretical Aspects of Computer Software, 4th International Symposium, TACS 2001, Sendai, Japan, October 29-31, 2001, Proceedings, pp. 298-315, 2001, Springer, 3-540-42736-8. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
EUROCAST ![In: Computer Aided Systems Theory - EUROCAST 2001, Las Palmas de Gran Canaria, Spain, February 19-23, 2001, Revised Papers, pp. 583-596, 2001, Springer, 3-540-42959-X. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
37 | Ewen Denney |
A Prototype Proof Translator from HOL to Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Portland, Oregon, USA, August 14-18, 2000, Proceedings, pp. 108-125, 2000, Springer, 3-540-67863-8. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
37 | Herman Geuvers, Milad Niqui |
Constructive Reals in Coq: Axioms and Categoricity. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000, Selected Papers, pp. 79-95, 2000, Springer, 3-540-43287-6. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
37 | Solange Coupet-Grimal, Line Jakubiec |
Hardware Verification Using Co-induction in COQ. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs'99, Nice, France, September, 1999, Proceedings, pp. 91-108, 1999, Springer, 3-540-66463-7. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
37 | David Delahaye |
Information Retrieval in a Coq Proof Library Using Type Isomorphisms. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, International Workshop TYPES'99, Lökeberg, Sweden, June 12-16, 1999, Selected Papers, pp. 131-147, 1999, Springer, 3-540-41517-3. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
37 | Christoph Sprenger 0001 |
A Verified Model Checker for the Modal µ-calculus in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TACAS ![In: Tools and Algorithms for Construction and Analysis of Systems, 4th International Conference, TACAS '98, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'98, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings, pp. 167-183, 1998, Springer, 3-540-64356-7. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 40(4), pp. 307-326, 2008. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Manag. Sci. ![In: Manag. Sci. 67(10), pp. 6294-6316, 2021. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Access ![In: IEEE Access 9, pp. 122607-122617, 2021. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Sensors ![In: Sensors 21(4), pp. 1438, 2021. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
BIODEVICES ![In: Proceedings of the 14th International Joint Conference on Biomedical Engineering Systems and Technologies, BIOSTEC 2021, Volume 1: BIODEVICES, Online Streaming, February 11-13, 2021., pp. 49-57, 2021, SCITEPRESS, 978-989-758-490-9. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Access ![In: IEEE Access 8, pp. 117245-117252, 2020. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IBM J. Res. Dev. ![In: IBM J. Res. Dev. 64(5/6), pp. 14:1-14:13, 2020. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Int. J. Agric. Environ. Inf. Syst. ![In: Int. J. Agric. Environ. Inf. Syst. 8(3), pp. 1-20, 2017. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
34 | Pascal Masselin, Eugene Bychkov, David Le Coq |
New strategy for direct laser writing of low loss waveguide. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICTON ![In: 2017 19th International Conference on Transparent Optical Networks (ICTON), Girona, Spain, July 2-6, 2017, pp. 1-4, 2017, IEEE, 978-1-5386-0859-3. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
M&N ![In: IEEE International Workshop on Measurement and Networking, M&N 2017, Naples, Italy, September 27-29, 2017, pp. 1-4, 2017, IEEE, 978-1-5090-5679-8. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICTON ![In: 17th International Conference on Transparent Optical Networks, ICTON 2015, Budapest, Hungary, July 5-9, 2015, pp. 1-4, 2015, IEEE, 978-1-4673-7880-2. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
COMPSAC Workshops ![In: 39th Annual Computer Software and Applications Conference, COMPSAC Workshops 2015, Taichung, Taiwan, July 1-5, 2015, pp. 164-169, 2015, IEEE Computer Society. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Instrum. Meas. ![In: IEEE Trans. Instrum. Meas. 62(6), pp. 1568-1573, 2013. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Int. J. Medical Informatics ![In: Int. J. Medical Informatics 81(4), pp. 244-256, 2012. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Softw. ![In: IEEE Softw. 29(3), pp. 64-70, 2012. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Inf. Softw. Technol. ![In: Inf. Softw. Technol. 54(6), pp. 569-590, 2012. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Microelectron. Reliab. ![In: Microelectron. Reliab. 51(6), pp. 1060-1068, 2011. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISSCC ![In: IEEE International Solid-State Circuits Conference, ISSCC 2011, Digest of Technical Papers, San Francisco, CA, USA, 20-24 February, 2011, pp. 382-384, 2011, IEEE, 978-1-61284-303-2. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Ada-Europe ![In: Reliable Software Technologies - Ada-Europe 2011 - 16th Ada-Europe International Conference on Reliable Software Technologies, Edinburgh, UK, June 20-24, 2011. Proceedings, pp. 61-74, 2011, Springer, 978-3-642-21337-3. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Microelectron. Reliab. ![In: Microelectron. Reliab. 50(7), pp. 1007-1013, 2010. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICST ![In: Third International Conference on Software Testing, Verification and Validation, ICST 2010, Paris, France, April 7-9, 2010, pp. 335-344, 2010, IEEE Computer Society, 978-0-7695-3990-4. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
34 | Guilhem Coq, X. Li, Olivier Alata, Yannis Pousset, Christian Olivier |
Law recognition via histogram-based estimation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICASSP ![In: Proceedings of the IEEE International Conference on Acoustics, Speech, and Signal Processing, ICASSP 2009, 19-24 April 2009, Taipei, Taiwan, pp. 3425-3428, 2009, IEEE. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
2008 |
RDF |
|
34 | Guilhem Coq, Olivier Alata, Marc Arnaudon, Christian Olivier |
Information Criteria and Arithmetic Codings : An Illustration on Raw Images ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/0706.1700, 2007. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Sci. Comput. ![In: J. Sci. Comput. 31(3), pp. 419-458, 2007. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
EUSIPCO ![In: 15th European Signal Processing Conference, EUSIPCO 2007, Poznan, Poland, September 3-7, 2007, pp. 634-638, 2007, IEEE, 978-839-2134-04-6. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
EGC ![In: Extraction et gestion des connaissances (EGC'2002), Actes des deuxièmes journées Extraction et Gestion des Connaissances, Montpellier, France, 21-23 janvier 2002, pp. 203-220, 2002, Hermes Science Publications, 2-7462-0406-1. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP BibTeX RDF |
|
32 | François Garillot, Georges Gonthier, Assia Mahboubi, Laurence Rideau |
Packaging Mathematical Structures. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, pp. 327-342, 2009, Springer, 978-3-642-03358-2. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, pp. 293-309, 2009, Springer, 978-3-642-03358-2. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
sequential game theory, effective generalisation, abstraction, induction, Coq |
32 | Jean Goubault-Larrecq |
Towards Producing Formally Checkable Security Proofs, Automatically. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CSF ![In: Proceedings of the 21st IEEE Computer Security Foundations Symposium, CSF 2008, Pittsburgh, Pennsylvania, USA, 23-25 June 2008, pp. 224-238, 2008, IEEE Computer Society, 978-0-7695-3182-3. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, International Conference, TYPES 2008, Torino, Italy, March 26-29, 2008, Revised Selected Papers, pp. 220-236, 2008, Springer, 978-3-642-02443-6. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 39(2), pp. 161-180, 2007. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
EUROCAST ![In: Computer Aided Systems Theory - EUROCAST 2007, 11th International Conference on Computer Aided Systems Theory, Las Palmas de Gran Canaria, Spain, February 12-16, 2007, Revised Selected Papers, pp. 282-289, 2007, Springer, 978-3-540-75866-2. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FME ![In: FME '97: Industrial Applications and Strengthened Foundations of Formal Methods, 4th International Symposium of Formal Methods Europe, Graz, Austria, September 15-19, 1997, Proceedings, pp. 358-377, 1997, Springer, 3-540-63533-5. The full citation details ...](Pics/full.jpeg) |
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). ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
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). ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
2023 |
RDF |
|
32 | Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters |
Extracting functional programs from Coq, in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Funct. Program. ![In: J. Funct. Program. 32, pp. e11, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
32 | Mario Frank 0002 |
The Coq Proof Script Visualiser (coq-psv). ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2101.07761, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP BibTeX RDF |
|
32 | Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters |
Extracting functional programs from Coq, in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2108.02995, 2021. The full citation details ...](Pics/full.jpeg) |
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)). ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
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). ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
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). ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
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). ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
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). ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
2020 |
RDF |
|
32 | Enrico Tassi |
Deriving Proved Equality Tests in Coq-Elpi: Stronger Induction Principles for Containers in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA., pp. 29:1-29:18, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-122-1. The full citation details ...](Pics/full.jpeg) |
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). ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
2019 |
RDF |
|
32 | Guillaume Claret |
Program in Coq. (Programmer en Coq). ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
2018 |
RDF |
|
32 | Jean-Pierre Jouannaud, Pierre-Yves Strub |
Coq without Type Casts: A Complete Proof of Coq Modulo Theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LPAR ![In: LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017, pp. 474-489, 2017, EasyChair. The full citation details ...](Pics/full.jpeg) |
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). ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
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). ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
2015 |
RDF |
|
32 | Jaime Gaspar |
Short Introduction by Example to Coq and Formalising ZF ⊆ ZFε in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CICM Workshops ![In: Joint Proceedings of the MathUI, OpenMath and ThEdu Workshops and Work in Progress track at CICM co-located with Conferences on Intelligent Computer Mathematics (CICM 2014), Coimbra, Portugal, July 7-11, 2014., 2014, CEUR-WS.org. The full citation details ...](Pics/full.jpeg) |
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). ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
2014 |
RDF |
|
Displaying result #1 - #100 of 959 (100 per page; Change: ) Pages: [ 1][ 2][ 3][ 4][ 5][ 6][ 7][ 8][ 9][ 10][ >>] |
|