|
|
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 |
16 | Thibault Hilaire, David Ilcinkas, Jérôme Leroux |
A State-of-the-Art Karp-Miller Algorithm Certified in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TACAS (1) ![In: Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I, pp. 370-389, 2024, Springer, 978-3-031-57245-6. The full citation details ...](Pics/full.jpeg) |
2024 |
DBLP DOI BibTeX RDF |
|
16 | Andrew W. Appel, Ariel Kellison |
VCFloat2: Floating-Point Error Analysis in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, London, UK, January 15-16, 2024, pp. 14-29, 2024, ACM. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, London, UK, January 15-16, 2024, pp. 230-245, 2024, ACM. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Proc. ACM Program. Lang. ![In: Proc. ACM Program. Lang. 7(POPL), pp. 1770-1800, January 2023. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Proc. ACM Program. Lang. ![In: Proc. ACM Program. Lang. 7(POPL), pp. 61-90, January 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
16 | David Nowak, Vlad Rusu |
While Loops in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FROM ![In: Proceedings 7th Symposium on Working Formal Methods, FROM 2023, Bucharest, Romania, 21-22 September 2023., pp. 96-109, 2023. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2305.02521, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
16 | Andrei Aleksandrov, Kim Völlinger |
Formalizing Piecewise Affine Activation Functions of Neural Networks in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2301.12893, 2023. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2310.06376, 2023. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2311.10965, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
16 | Zachary Flores, Angelo Taranto, Eric Bond, Yakir Forman |
A Formalization of Operads in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2303.08894, 2023. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FROM ![In: Proceedings 7th Symposium on Working Formal Methods, FROM 2023, Bucharest, Romania, 21-22 September 2023., pp. 80-95, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
16 | Xinyi Wan, Ke Xu, Qinxiang Cao |
Coq Formalization of ZFC Set Theory for Teaching Scenarios. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Int. J. Softw. Informatics ![In: Int. J. Softw. Informatics 13(3), pp. 323-357, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
16 | Dominik Kirst, Marc Hermes |
Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 67(1), pp. 13, March 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
16 | Érik Martin-Dorel, Guillaume Melquiond, Pierre Roux |
Enabling Floating-Point Arithmetic in the Coq Proof Assistant. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 67(4), pp. 33, December 2023. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM Trans. Program. Lang. Syst. ![In: ACM Trans. Program. Lang. Syst. 45(3), pp. 15:1-15:61, September 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
16 | Jonathan Chan, Yufeng Li, William J. Bowman |
Is sized typing for Coq practical? ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Funct. Program. ![In: J. Funct. Program. 33, pp. e1, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
16 | Olivier Danvy |
Fold-unfold lemmas for reasoning about recursive programs using the Coq proof assistant - ERRATUM. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Funct. Program. ![In: J. Funct. Program. 33, pp. e3, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
16 | ZhengPu Shi, GuoJun Xie, Gang Chen |
CoqMatrix: Formal matrix library with multiple models in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Syst. Archit. ![In: J. Syst. Archit. 143, pp. 102986, October 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
16 | Frédéric Loulergue, Jolan Philippe |
Towards Verified Scalable Parallel Computing with Coq and Spark. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FTfJP@ECOOP ![In: Proceedings of the 25th ACM International Workshop on Formal Techniques for Java-like Programs, FTfJP 2023, Seattle, WA, USA, 18 July 2023, pp. 11-17, 2023, ACM. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LPAR ![In: LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Manizales, Colombia, 4-9th June 2023., pp. 11-22, 2023, EasyChair. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
16 | Jan Tusil, Péter Bereczky, Dániel Horpácsi |
Interactive Matching Logic Proofs in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICTAC ![In: Theoretical Aspects of Computing - ICTAC 2023 - 20th International Colloquium, Lima, Peru, December 4-8, 2023, Proceedings, pp. 139-157, 2023, Springer, 978-3-031-47962-5. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FM ![In: Formal Methods - 25th International Symposium, FM 2023, Lübeck, Germany, March 6-10, 2023, Proceedings, pp. 39-55, 2023, Springer, 978-3-031-27480-0. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Theories of Programming and Formal Methods ![In: Theories of Programming and Formal Methods - Essays Dedicated to Jifeng He on the Occasion of His 80th Birthday, pp. 395-412, 2023, Springer, 978-3-031-40435-1. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
16 | Ayumu Saito, Reynald Affeldt |
Experimenting with an Intrinsically-Typed Probabilistic Programming Language in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
APLAS ![In: Programming Languages and Systems - 21st Asian Symposium, APLAS 2023, Taipei, Taiwan, November 26-29, 2023, Proceedings, pp. 182-202, 2023, Springer, 978-981-99-8310-0. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
16 | Giorgio Audrito, Daniel Haures |
Combining Static and Runtime Verification with AC and Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
VORTEX@ISSTA ![In: Proceedings of the 6th International Workshop on Verification and Monitoring at Runtime Execution, VORTEX 2023, Seattle, WA, USA, 18 July 2023, pp. 17-20, 2023, ACM. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
16 | Xupeng Li, Xuheng Li, Wei Qiang, Ronghui Gu, Jason Nieh |
Spoq: Scaling Machine-Checkable Systems Verification in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
OSDI ![In: 17th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2023, Boston, MA, USA, July 10-12, 2023., pp. 851-869, 2023, USENIX Association. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP BibTeX RDF |
|
16 | Dominique Larchey-Wendling, Jean-François Monin |
Proof Pearl: Faithful Computation and Extraction of μ-Recursive Algorithms in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 21:1-21:17, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 12:1-12:18, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 25:1-25:19, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
16 | Reynald Affeldt, Cyril Cohen, Ayumu Saito |
Semantics of Probabilistic Programs using s-Finite Kernels in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, Boston, MA, USA, January 16-17, 2023, pp. 3-16, 2023, ACM. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, Boston, MA, USA, January 16-17, 2023, pp. 167-181, 2023, ACM. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
16 | Eske Hoy Nielsen, Danil Annenkov, Bas Spitters |
Formalising Decentralised Exchanges in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, Boston, MA, USA, January 16-17, 2023, pp. 290-302, 2023, ACM. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
16 | Andrei Aleksandrov, Kim Völlinger |
Formalizing Piecewise Affine Activation Functions of Neural Networks in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
NFM ![In: NASA Formal Methods - 15th International Symposium, NFM 2023, Houston, TX, USA, May 16-18, 2023, Proceedings, pp. 62-78, 2023, Springer, 978-3-031-33169-5. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CSL ![In: 31st EACSL Annual Conference on Computer Science Logic, CSL 2023, February 13-16, 2023, Warsaw, Poland., pp. 21:1-21:21, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-264-8. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FroCoS ![In: Frontiers of Combining Systems - 14th International Symposium, FroCoS 2023, Prague, Czech Republic, September 20-22, 2023, Proceedings, pp. 41-59, 2023, Springer, 978-3-031-43368-9. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Proc. ACM Program. Lang. ![In: Proc. ACM Program. Lang. 6(OOPSLA1), pp. 1-27, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
16 | Vlad Rusu, David Nowak |
Defining Corecursive Functions in Coq Using Approximations (Artifact). ![Search on Bibsonomy](Pics/bibsonomy.png) |
Dagstuhl Artifacts Ser. ![In: Dagstuhl Artifacts Ser. 8(2), pp. 02:1-02:2, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
16 | Sylvie Boldo, François Clément, Louise Leclerc |
A Coq Formalization of the Bochner integral. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2201.03242, 2022. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2202.05040, 2022. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FROM ![In: Proceedings of the Sixth Working Formal Methods Symposium, FROM 2022, `Al. I. Cuza University`, Iasi, Romania, 19-20 September, 2022., pp. 17-36, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
16 | Catherine Dubois, Nicolas Magaud, Alain Giorgetti |
Pragmatic isomorphism proofs between Coq representations: application to lambda-term families. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2212.10453, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
16 | Karl Palmskog, Enrico Tassi, Théo Zimmermann |
Reliably Reproducing Machine-Checked Proofs with the Coq Platform. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2203.09835, 2022. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2202.13823, 2022. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2203.08941, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
16 | Ana de Almeida Borges |
Towards a Coq formalization of a quantified modal logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2206.03358, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
16 | Eske Hoy Nielsen, Danil Annenkov, Bas Spitters |
Formalising Decentralised Exchanges in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2203.08016, 2022. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2209.14227, 2022. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2211.06863, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
16 | Dominique Larchey-Wendling, Yannick Forster 0002 |
Hilbert's Tenth Problem in Coq (Extended Version). ![Search on Bibsonomy](Pics/bibsonomy.png) |
Log. Methods Comput. Sci. ![In: Log. Methods Comput. Sci. 18(1), 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
16 | Dominik Kirst, Dominique Larchey-Wendling |
Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Log. Methods Comput. Sci. ![In: Log. Methods Comput. Sci. 18(2), 2022. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 66(2), pp. 175-213, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
16 | Olivier Danvy |
Fold-unfold lemmas for reasoning about recursive programs using the Coq proof assistant. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Funct. Program. ![In: J. Funct. Program. 32, pp. e13, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
16 | Avraham Shinnar, Barry M. Trager |
General Probability in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
DSN Workshops ![In: 52nd Annual IEEE/IFIP International Conference on Dependable Systems and Networks, DSN Workshops 2022, Baltimore, MD, USA, June 27-30, 2022, pp. 70-71, 2022, IEEE, 978-1-6654-0262-0. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MEMOCODE ![In: 20th ACM-IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2022, Shanghai, China, October 13-14, 2022, pp. 1-9, 2022, IEEE, 979-8-3503-3190-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
16 | Joshua M. Cohen, Qinshi Wang, Andrew W. Appel |
Verified Erasure Correction in Coq with MathComp and VST. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CAV (2) ![In: Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part II, pp. 272-292, 2022, Springer, 978-3-031-13187-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
16 | Felipe Lisboa Malaquias, Mihail Asavoae, Florian Brandner |
A Coq Framework for More Trustworthy DRAM Controllers. ![Search on Bibsonomy](Pics/bibsonomy.png) |
RTNS ![In: RTNS 2022: The 30th International Conference on Real-Time Networks and Systems, Paris, France, June 7 - 8, 2022, pp. 140-150, 2022, ACM, 978-1-4503-9650-9. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
16 | Ayumu Saito, Reynald Affeldt |
Towards a Practical Library for Monadic Equational Reasoning in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MPC ![In: Mathematics of Program Construction - 14th International Conference, MPC 2022, Tbilisi, Georgia, September 26-28, 2022, Proceedings, pp. 151-177, 2022, Springer, 978-3-031-16911-3. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SBLP ![In: SBLP 2022: XXVI Brazilian Symposium on Programming Languages, Virtual Event Brazil, October 6 - 7, 2022, pp. 1-7, 2022, ACM, 978-1-4503-9744-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
16 | Catherine Dubois, Nicolas Magaud, Alain Giorgetti |
Pragmatic Isomorphism Proofs Between Coq Representations: Application to Lambda-Term Families. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 28th International Conference on Types for Proofs and Programs, TYPES 2022, June 20-25, 2022, LS2N, University of Nantes, France, pp. 11:1-11:19, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-285-3. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
16 | Vlad Rusu, David Nowak |
Defining Corecursive Functions in Coq Using Approximations. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ECOOP ![In: 36th European Conference on Object-Oriented Programming, ECOOP 2022, June 6-10, 2022, Berlin, Germany., pp. 12:1-12:24, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-225-9. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
16 | Ana de Almeida Borges |
Towards a Coq Formalization of a Quantified Modal Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ARQNL@IJCAR ![In: Proceedings of the 4th International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2022) affiliated with the 11th International Joint Conference on Automated Reasoning (IJCAR 2022), Haifa, Israel, August 11, 2022., pp. 13-27, 2022, CEUR-WS.org. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
RTSS ![In: IEEE Real-Time Systems Symposium, RTSS 2022, Houston, TX, USA, December 5-8, 2022, pp. 197-210, 2022, IEEE, 978-1-6654-5346-2. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
16 | Conor Reynolds, Rosemary Monahan |
Machine-Assisted Proofs for Institutions in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IFM ![In: Integrated Formal Methods - 17th International Conference, IFM 2022, Lugano, Switzerland, June 7-10, 2022, Proceedings, pp. 369-372, 2022, Springer, 978-3-031-07726-5. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel., pp. 25:1-25:17, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-252-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
16 | Malgorzata Biernacka, Witold Charatonik, Tomasz Drab |
The Zoo of Lambda-Calculus Reduction Strategies, And Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel., pp. 7:1-7:19, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-252-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
16 | Johannes Hostert, Andrej Dudenhefner, Dominik Kirst |
Undecidability of Dyadic First-Order Logic in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel., pp. 19:1-19:19, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-252-5. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel., pp. 18:1-18:18, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-252-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
16 | Yannick Forster 0002, Fabian Kunze, Nils Lauermann |
Synthetic Kolmogorov Complexity in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel., pp. 12:1-12:19, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-252-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
16 | Yichen Tao, Qinxiang Cao |
LOGIC: A Coq Library for Logics. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SETTA ![In: Dependable Software Engineering. Theories, Tools, and Applications - 8th International Symposium, SETTA 2022, Beijing, China, October 27-29, 2022, Proceedings, pp. 205-226, 2022, Springer, 978-3-031-21212-3. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
16 | ZhengPu Shi, Gang Chen |
Integration of Multiple Formal Matrix Models in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SETTA ![In: Dependable Software Engineering. Theories, Tools, and Applications - 8th International Symposium, SETTA 2022, Beijing, China, October 27-29, 2022, Proceedings, pp. 169-186, 2022, Springer, 978-3-031-21212-3. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
16 | Dan Frumin |
Semantic cut elimination for the logic of bunched implications, formalized in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022, pp. 291-306, 2022, ACM, 978-1-4503-9182-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
16 | Mark Koch, Dominik Kirst |
Undecidability, incompleteness, and completeness of second-order logic in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022, pp. 274-290, 2022, ACM, 978-1-4503-9182-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
16 | Andrew W. Appel |
Coq's vibrant ecosystem for verification engineering (invited talk). ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022, pp. 2-11, 2022, ACM, 978-1-4503-9182-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
16 | Conor Reynolds, Rosemary Monahan |
Machine-Assisted Proofs for Institutions in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TASE ![In: Theoretical Aspects of Software Engineering - 16th International Symposium, TASE 2022, Cluj-Napoca, Romania, July 8-10, 2022, Proceedings, pp. 180-196, 2022, Springer, 978-3-031-10362-9. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
16 | Wenjun Shi, Qinxiang Cao, Yuxin Deng, Hanru Jiang, Yuan Feng 0001 |
Symbolic Reasoning About Quantum Circuits in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Comput. Sci. Technol. ![In: J. Comput. Sci. Technol. 36(6), pp. 1291-1306, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
16 | Yezhou Liu, Radu Nicolescu, Jing Sun 0002 |
Formal verification of cP systems using Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Membr. Comput. ![In: J. Membr. Comput. 3(3), pp. 205-220, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
16 | Luís Cruz-Filipe, Fabrizio Montesi, Marco Peressotti |
Formalising a Turing-Complete Choreographic Language in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2102.02627, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP BibTeX RDF |
|
16 | François Clément, Vincent Martin |
Lebesgue integration. Detailed proofs to be formalized in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2101.05678, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP BibTeX RDF |
|
16 | Deivid Vale, Niels van der Weide |
Formalizing Higher-Order Termination in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2112.05715, 2021. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2104.05256, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP BibTeX RDF |
|
16 | Elizabeth Dietrich |
A beginner guide to Iris, Coq and separation logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2105.12077, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP BibTeX RDF |
|
16 | Dan Frumin |
Semantic Cut Elimination for the Logic of Bunched Implications, Formalized in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2112.05515, 2021. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2104.05207, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP BibTeX RDF |
|
16 | Nicolas Magaud |
Integrating an Automated Prover for Projective Geometry as a New Tactic in the Coq Proof Assistant. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PxTP ![In: Proceedings Seventh Workshop on Proof eXchange for Theorem Proving, PxTP 2021, Pittsburg, PA, USA, July 11, 2021., pp. 40-47, 2021. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings of the Sixteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2021, Pittsburgh, USA, 16th July 2021., pp. 71-87, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
16 | Dominik Kirst, Dominique Larchey-Wendling |
Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2104.14445, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP BibTeX RDF |
|
16 | Valentin Blot, Louise Dubois de Prisque, Chantal Keller, Pierre Vial |
General Automation in Coq through Modular Transformations. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PxTP ![In: Proceedings Seventh Workshop on Proof eXchange for Theorem Proving, PxTP 2021, Pittsburg, PA, USA, July 11, 2021., pp. 24-39, 2021. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2103.01346, 2021. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2106.12973, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP BibTeX RDF |
|
16 | Florian Steinberg 0001, Laurent Théry, Holger Thies |
Computable analysis and notions of continuity in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Log. Methods Comput. Sci. ![In: Log. Methods Comput. Sci. 17(2), 2021. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IACR Cryptol. ePrint Arch. ![In: IACR Cryptol. ePrint Arch. 2021, pp. 397, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP BibTeX RDF |
|
16 | Peter Schwabe, Benoît Viguier, Timmy Weerwag, Freek Wiedijk |
A Coq proof of the correctness of X25519 in TweetNaCl. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IACR Cryptol. ePrint Arch. ![In: IACR Cryptol. ePrint Arch. 2021, pp. 428, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP BibTeX RDF |
|
16 | Guillaume Ambal, Sergueï Lenglet, Alan Schmitt |
HOπ in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 65(1), pp. 75-124, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
16 | Raul Fervari, Francisco Trucco, Beta Ziliani |
Verification of dynamic bisimulation theorems in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Log. Algebraic Methods Program. ![In: J. Log. Algebraic Methods Program. 120, pp. 100642, 2021. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Sci. Comput. Program. ![In: Sci. Comput. Program. 201, pp. 102537, 2021. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Funct. Program. ![In: J. Funct. Program. 31, pp. e5, 2021. The full citation details ...](Pics/full.jpeg) |
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). ![Search on Bibsonomy](Pics/bibsonomy.png) |
FMBC@CAV ![In: 3rd International Workshop on Formal Methods for Blockchains, FMBC@CAV 2021, July 18-19, 2021, Los Angeles, California, USA (Virtual Conference)., pp. 3:1-3:8, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-209-9. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
16 | Akira Tanaka |
Coq to C translation with partial evaluation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PEPM@POPL ![In: Proceedings of the 2021 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM@POPL 2021, Virtual Event, Denmark, January 18-19, 2021., pp. 14-31, 2021, ACM, 978-1-4503-8305-9. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
16 | Xiaokun Luan, Xiyue Zhang, Meng Sun 0002 |
Using LSTM to Predict Tactics in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SEKE ![In: The 33rd International Conference on Software Engineering and Knowledge Engineering, SEKE 2021, KSIR Virtual Conference Center, USA, July 1 - July 10, 2021., pp. 132-137, 2021, KSI Research Inc., 1-891706-52-7. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
Displaying result #201 - #300 of 959 (100 per page; Change: ) Pages: [ <<][ 1][ 2][ 3][ 4][ 5][ 6][ 7][ 8][ 9][ 10][ >>] |
|