References

  1. Andreas Abel, Joakim Öhman & Andrea Vezzosi (2018): Decidability of conversion for type theory in type theory. PACMPL 2(POPL), pp. 23:1–23:29, doi:10.1145/3158111.
  2. Behzad Akbarpour, Amr T. Abdel-Hamid, Sofiène Tahar & John Harrison (2010): Verifying a Synthesized Implementation of IEEE-754 Floating-Point Exponential Function using HOL. Comput. J. 53(4), pp. 465–488, doi:10.1093/comjnl/bxp023.
  3. Thorsten Altenkirch (1993): Constructions, Inductive Types and Strong Normalization. University of Edinburgh.
  4. Abhishek Anand, Andrew Appel, Greg Morrisett, Zoe Paraskevopoulou, Randy Pollack, Olivier Savary Belanger, Matthieu Sozeau & Matthew Weaver (2017): CertiCoq: A verified compiler for Coq. In: CoqPL, Paris, France.
  5. Andrew W. Appel (2014): Program Logics - for Certified Compilers. Cambridge University Press, doi:10.1017/CBO9781107256552.
  6. Michaël Armand, Benjamin Grégoire, Arnaud Spiwack & Laurent Théry (2010): Extending Coq with Imperative Features and Its Application to SAT Verification. In: Matt Kaufmann & Lawrence C. Paulson: Interactive Theorem Proving. Springer, pp. 83–98, doi:10.1016/j.jal.2007.07.003.
  7. Bruno Barras (1999): Auto-validation d'un système de preuves avec familles inductives. Thèse de doctorat. Université Paris 7.
  8. Bruno Barras (2012): Semantical Investigations in Intuitionistic Set Theory and Type Theories with Inductive Families. Unpublished.
  9. Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau & Bas Spitters (2017): The HoTT library: a formalization of homotopy type theory in Coq. In: Yves Bertot & Viktor Vafeiadis: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017. ACM, pp. 164–172, doi:10.1145/3018610.3018615.
  10. Michael A. Bender, Jeremy T. Fineman, Seth Gilbert & Robert E. Tarjan (2016): A New Approach to Incremental Cycle Detection and Related Problems. ACM Trans. Algorithms 12(2), pp. 14:1–14:22, doi:10.1145/2756553.
  11. Guillaume Bertholon, Érik Martin-Dorel & Pierre Roux (2019): Primitive Floats in Coq. In: John Harrison, John O'Leary & Andrew Tolmach: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA, LIPIcs 141. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 7:1–7:20, doi:10.4230/LIPIcs.ITP.2019.7.
  12. Marcel Ullrich Bohdan Liesnikov & Yannick Forster (2020): Generating induction principles and subterm relations for inductive types using MetaCoq. The Coq Workshop 2020.
  13. James Chapman (2009): Type Theory Should Eat Itself. Electron. Notes Theor. Comput. Sci. 228, pp. 21–36, doi:10.1016/j.entcs.2008.12.114.
  14. Adam Chlipala (2020): Proof assistants at the hardware-software interface (invited talk). In: Jasmin Blanchette & Catalin Hritcu: CPP 2020. ACM, pp. 2, doi:10.1145/3372885.3378575.
  15. Thierry Coquand & Gérard Huet (1988): The Calculus of Constructions. Information and Computation 76(2–3), pp. 95–120, doi:10.1016/0890-5401(88)90005-3.
  16. Jean-Christophe Filliâtre (2000): Design of a proof assistant: Coq version 7. Research Report. Université Paris-Sud.
  17. Jean-Christophe Filliâtre (2020): A Coq retrospective, at the heart of Coq architecture, the genesis of version 7.0. Invited talk at the Coq Workshop 2020.
  18. Gallium, Marelle, CEDRIC & PPS (2008): The CompCert project. Compilers You Can Formally Trust.
  19. Eduardo Giménez (1998): Structural Recursive Definitions in Type Theory. In: Kim Guldstrand Larsen, Sven Skyum & Glynn Winskel: ICALP, LNCS 1443. Springer, pp. 397–408.
  20. Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O'Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi & Laurent Théry (2013): A Machine-Checked Proof of the Odd Order Theorem. In: Sandrine Blazy, Christine Paulin-Mohring & David Pichardie: ITP 2013, LNCS 7998. Springer, pp. 163–179, doi:10.1007/978-3-642-39634-2.08emwidth.35em height.6pt.08em14.
  21. Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sjöberg & David Costanzo (2016): CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In: Kimberly Keeton & Timothy Roscoe: 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016, Savannah, GA, USA, November 2-4, 2016. USENIX Association, pp. 653–669, doi:10.5555/3026877.3026928.
  22. Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud & François Pottier (2019): Formal Proof and Analysis of an Incremental Cycle Detection Algorithm. In: ITP 2019 - 10th Conference on Interactive Theorem Proving, Portland, United States.
  23. Thomas C. Hales, Mark Adams, Gertrud Bauer, Dat Tat Dang, John Harrison, Truong Le Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Thang Tat Nguyen, Truong Quang Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason M. Rute, Alexey Solovyev, An Hoai Thi Ta, Trung Nam Tran, Diep Thi Trieu, Josef Urban, Ky Khac Vu & Roland Zumkeller (2015): A formal proof of the Kepler conjecture. CoRR abs/1501.02155.
  24. John Harrison (2006): Towards self-verification of HOL Light. In: Ulrich Furbach & Natarajan Shankar: Proceedings of the third International Joint Conference, IJCAR 2006, LNCS 4130. Springer-Verlag, Seattle, WA, pp. 177–191.
  25. Hugo Herbelin (2005): Type Inference with Algebraic Universes in the Calculus of Inductive Constructions. Manuscript.
  26. Simon Huber (2019): Canonicity for Cubical Type Theory. Journal of Automated Reasoning 63(2), pp. 173–210, doi:10.1007/s10817-018-9469-1.
  27. Guilhem Jaber, Gabriel Lewertowski, Pierre-Marie Pédrot, Matthieu Sozeau & Nicolas Tabareau (2016): The Definitional Side of the Forcing. In: Martin Grohe, Eric Koskinen & Natarajan Shankar: LICS '16. ACM, pp. 367–376, doi:10.1145/2933575.2935320.
  28. Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers & Derek Dreyer (2021): Safe systems programming in Rust. Commun. ACM 64(4), pp. 144–152, doi:10.1145/3418295.
  29. Jan-Oliver Kaiser, Beta Ziliani, Robbert Krebbers, Yann Régis-Gianas & Derek Dreyer (2018): Mtac2: typed tactics for backward reasoning in Coq. PACMPL 2(ICFP), pp. 78:1–78:31, doi:10.1145/3236773.
  30. Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch & Simon Winwood (2009): seL4: formal verification of an OS kernel. In: Jeanna Neefe Matthews & Thomas E. Anderson: SOSP. ACM, pp. 207–220, doi:10.1145/1629575.1629596.
  31. Ramana Kumar, Rob Arthan, Magnus O. Myreen & Scott Owens (2016): Self-Formalisation of Higher-Order Logic - Semantics, Soundness, and a Verified Implementation. J. Autom. Reason. 56(3), pp. 221–259, doi:10.1007/s10817-015-9357-x.
  32. Meven Lennon-Bertrand (2021): Complete Bidirectional Typing for the Calculus of Inductive Constructions. In: Liron Cohen & Cezary Kaliszyk: ITP 2021, LIPIcs 193. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 24:1–24:19, doi:10.4230/LIPIcs.ITP.2021.24.
  33. Xavier Leroy (2006): Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: 33rd symposium Principles of Programming Languages. ACM Press, pp. 42–54.
  34. Pierre Letouzey (2002): A New Extraction for Coq.. In: Herman Geuvers & Freek Wiedijk: TYPES'02, LNCS 2646. Springer, pp. 200–219.
  35. Pierre Letouzey (2004): Programmation fonctionnelle certifiée: l'extraction de programmes dans l'assistant Coq. Thèse de doctorat. Université Paris-Sud.
  36. Andreas Lööw, Ramana Kumar, Yong Kiam Tan, Magnus O. Myreen, Michael Norrish, Oskar Abrahamsson & Anthony Fox (2019): Verified Compilation on a Verified Processor. In: PLDI 2019. ACM, New York, NY, USA, pp. 1041–1053, doi:10.1145/3314221.3314622.
  37. Gregory Michael Malecha (2014): Extensible Proof Engineering in Intensional Type Theory. Harvard University.
  38. Christine Paulin-Mohring (1993): Inductive Definitions in the System Coq - Rules and Properties. In: Marc Bezem & Jan Friso Groote: Typed Lambda Calculi and Applications, doi:10.1007/BFb0037116.
  39. Pierre-Marie Pédrot & Nicolas Tabareau (2017): An effectful way to eliminate addiction to dependence. In: LICS 2017. IEEE Computer Society, pp. 1–12, doi:10.1109/LICS.2017.8005113.
  40. Pierre-Marie Pédrot & Nicolas Tabareau (2020): The fire triangle: how to mix substitution, dependent elimination, and effects. Proc. ACM Program. Lang. 4(POPL), pp. 58:1–58:28, doi:10.1145/3371126.
  41. Steven Schäfer, Tobias Tebbi & Gert Smolka (2015): Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions. In: Christian Urban & Xingyuan Zhang: ITP 2015, LNCS 9236. Springer, pp. 359–374, doi:10.1007/978-3-319-22102-1.08emwidth.35em height.6pt.08em24.
  42. Vincent Siles & Hugo Herbelin (2012): Pure Type System conversion is always typable. J. Funct. Program. 22(2), pp. 153–180, doi:10.1017/S0956796812000044.
  43. Matthieu Sozeau (2007): Subset Coercions in Coq. In: Thorsten Altenkirch & Conor McBride: TYPES'06, LNCS 4502. Springer, pp. 237–252, doi:10.1007/978-3-540-74464-1_16.
  44. Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau & Théo Winterhalter (2020): The MetaCoq Project. Journal of Automated Reasoning 64(5), pp. 947–999, doi:10.1007/s10817-019-09540-0.
  45. Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau & Théo Winterhalter (2020): Coq Coq Correct! Verifying Typechecking and Erasure for Coq, in Coq. Proceedings of the ACM on Programming Languages 4(POPL), doi:10.1145/3371076.
  46. Matthieu Sozeau & Nicolas Tabareau (2014): Universe Polymorphism in Coq. In: Gerwin Klein & Ruben Gamboa: ITP 2014, LNCS 8558. Springer, pp. 499–514, doi:10.1007/978-3-319-08970-6_32.
  47. Kathrin Stark, Steven Schäfer & Jonas Kaiser (2019): Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector substitutions. In: Assia Mahboubi & Magnus O. Myreen: CPP 2019. ACM, pp. 166–180, doi:10.1145/3293880.3294101.
  48. Jonathan Sterling & Carlo Angiuli (2021): Normalization for Cubical Type Theory. CoRR abs/2101.11479.
  49. Masako Takahashi (1995): Parallel Reductions in lambda-Calculus. Inf. Comput. 118(1), pp. 120–127, doi:10.1006/inco.1995.1057.
  50. Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony C. J. Fox, Scott Owens & Michael Norrish (2019): The verified CakeML compiler backend. J. Funct. Program. 29, pp. e2, doi:10.1017/S0956796818000229.
  51. The Coq Development Team (2021): The Coq Proof Assistant, doi:10.5281/zenodo.4501022.
  52. Amin Timany & Matthieu Sozeau (2017): Consistency of the Predicative Calculus of Cumulative Inductive Constructions (pCuIC). Research Report RR-9105. KU Leuven, Belgium ; Inria Paris.
  53. Amin Timany & Matthieu Sozeau (2018): Cumulative Inductive Types In Coq. In: Hélène Kirchner: FSCD, LIPIcs 108, pp. 29:1–29:16, doi:10.4230/LIPIcs.FSCD.2018.29.
  54. Benjamin Werner (1997): Sets in types, types in sets. In: Martín Abadi & Takayasu Ito: Theoretical Aspects of Computer Software. Springer, pp. 530–546, doi:10.1007/BFb0014566.
  55. Théo Winterhalter (2020): Formalisation and Meta-Theory of Type Theory. Université de Nantes. 2020NANT4012.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org