diff --git a/papers.html b/papers.html index e8e656fa..34d909d2 100644 --- a/papers.html +++ b/papers.html @@ -3,23 +3,30 @@ "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> + + + Mathematical Components: Research Papers - - - - + + @@ -99,7 +191,7 @@ @licstart The following is the entire license notice for the JavaScript code in this tag. -Copyright (C) 2012-2013 Free Software Foundation, Inc. +Copyright (C) 2012-2017 Free Software Foundation, Inc. The JavaScript code in this tag is free software: you can redistribute it and/or modify it under the terms of the GNU @@ -148,10 +240,10 @@

Mathematical Components: Research Papers

Table of Contents

@@ -161,20 +253,13 @@

Table of Contents

venues:

@@ -183,291 +268,228 @@

Table of Contents

wiki.

-
-

Mathematics

-
+
+

Mathematics

+
    -
  • Florent Bréhard, Assia Mahboubi and Damien Pous. A certificate-based -approach to formally verified approximations. ITP 2019. pdf -
    • +
  • Florent Bréhard, Assia Mahboubi and Damien Pous. A certificate-based +approach to formally verified approximations. ITP 2019. pdf
  • Xavier Allamigeon, Ricardo D. Katz. -A formalization of convex polyhedra based on the simplex method. ITP 2017 -
    • +A formalization of convex polyhedra based on the simplex method. ITP 2017
  • Evmorfia-Iro Bartzia. -A Formalization of Elliptic Curves for Cryptography. PhD thesis, Université Paris-Saclay, 2017, pdf -
    • +A Formalization of Elliptic Curves for Cryptography. PhD thesis, Université Paris-Saclay, 2017, pdf
  • Guillaume Cano, Cyril Cohen, Maxime Dénès, Anders Mörtberg, Vincent Siles. Formalized linear algebra over Elementary Divisor Rings in Coq. -LMCS 12(2), 2016 -
    • +LMCS 12(2), 2016
  • Cyril Cohen, Boris Djalal. -Formalization of a newton series representation of polynomials. CPP 2016 -
    • +Formalization of a newton series representation of polynomials. CPP 2016
  • Ken'ichi Kuga, Manabu Hagiwara, Mitsuharu Yamamoto. -Formalization of Bing's Shrinking Method in Geometric Topology. CICM 2016 -
    • +Formalization of Bing's Shrinking Method in Geometric Topology. CICM 2016
  • Gallego Arias, Emilio Jesús, Pierre Jouvelot. -Adventures in the (not so) Complex Space. The 7th Coq Workshop, paper/code/slides, 2015 -
    • +Adventures in the (not so) Complex Space. The 7th Coq Workshop, paper/code/slides, 2015
  • Frédéric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote, Enrico Tassi. -A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3). ITP 2014 -
    • +A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3). ITP 2014
  • Cyril Cohen, Anders Mörtberg. -A Coq Formalization of Finitely Presented Modules. ITP 2014 -
    • +A Coq Formalization of Finitely Presented Modules. ITP 2014
  • Anders Mörtberg. -Formalizing Refinements and Constructive Algebra in Type Theory. PhD, 2014 -
    • +Formalizing Refinements and Constructive Algebra in Type Theory. PhD, 2014
  • Evmorfia-Iro Bartzia, Pierre-Yves Strub. -A Formal Library for Elliptic Curves in the Coq Proof Assistant. ITP 2014 -
    • +A Formal Library for Elliptic Curves in the Coq Proof Assistant. ITP 2014
  • Jónathan Heras, Thierry Coquand, Anders Mörtberg, Vincent Siles. -Computing persistent homology within Coq/SSReflect. ACM Trans. Comput. Log. 14(4), 2013 -
    • +Computing persistent homology within Coq/SSReflect. ACM Trans. Comput. Log. 14(4), 2013
  • 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. -A Machine-Checked Proof of the Odd Order Theorem. ITP 2013 -
    • +A Machine-Checked Proof of the Odd Order Theorem. ITP 2013
  • Maxime Dénès, Anders Mörtberg, Vincent Siles. -A Refinement-Based Approach to Computational Algebra in Coq. ITP 2012 -
    • +A Refinement-Based Approach to Computational Algebra in Coq. ITP 2012
  • Jónathan Heras, Maxime Dénès, Gadea Mata, Anders Mörtberg, María Poza, Vincent Siles. Towards a Certified Computation of Homology Groups for Digital Images. -Computational Topology in Image Context, 2012 -
    • +Computational Topology in Image Context, 2012
  • Assia Mahboubi, Cyril Cohen. Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination. -LMCS, 2012 -
    • +LMCS, 2012
  • Thierry Coquand, Anders Mörtberg, Vincent Siles. -Coherent and Strongly Discrete Rings in Type Theory. CPP 2012 -
    • +Coherent and Strongly Discrete Rings in Type Theory. CPP 2012
  • Cyril Cohen. Formalized algebraic numbers: construction and first-order theory. -PhD thesis, 2011 -
    • +PhD thesis, 2011
  • Jónathan Heras, María Poza, Maxime Dénès, Laurence Rideau. -Incidence Simplicial Matrices Formalized in Coq/SSReflect. Calculemus/MKM 2011: 30-44 -
    • +Incidence Simplicial Matrices Formalized in Coq/SSReflect. Calculemus/MKM 2011: 30-44
  • Georges Gonthier. -Point-Free, Set-Free Concrete Linear Algebra. ITP 2011 -
    • +Point-Free, Set-Free Concrete Linear Algebra. ITP 2011
-
-

Robotics

-
+
+

Robotics

+
  • Cyril Cohen, Damien Rouhling. -A Formal Proof in Coq of LaSalle's Invariance Principle. ITP 2017 -
    • +A Formal Proof in Coq of LaSalle's Invariance Principle. ITP 2017
  • Reynald Affeldt, Cyril Cohen. -Formal Foundations of 3D Geometry to Model Robot Manipulators. CPP 2017 -
    • +Formal Foundations of 3D Geometry to Model Robot Manipulators. CPP 2017
-
-

Programming and Algorithms

-
+
+

Programming and Algorithms

+
    +
  • Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, Kazunari Tanaka. +Proving tree algorithms for succinct data structures. +ITP 2019, pdf
  • Cyril Cohen, Damien Rouhling. -A refinement-based approach to large scale reflection for algebra. JFLA 2017 -
    • +A refinement-based approach to large scale reflection for algebra. JFLA 2017
  • Timmy Weerwag. Verifying an elliptic curve cryptographic algorithm_using Coq and the Ssreflect extension. -Master’s thesis, 2016 -
    • +Master’s thesis, 2016
  • Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis. -Mtac: A Monad for Typed Tactic Programming in Coq. Journal of Functional Programming, 2015 -
    • +Mtac: A Monad for Typed Tactic Programming in Coq. Journal of Functional Programming, 2015
  • Cyril Cohen, Maxime Dénès, Anders Mörtberg. -Refinements for free!. CPP 2013 -
    • +Refinements for free!. CPP 2013
  • Germán Andrés Delbianco, Aleksandar Nanevski. -Hoare-Style Reasoning with (Algebraic) Continuations. ICFP 2013 -
    • +Hoare-Style Reasoning with (Algebraic) Continuations. ICFP 2013
  • Andrew Kennedy, Nick Benton, Jonas B. Jensen, Pierre-Evariste Dagand. -Coq: the world's best macro assembler?. PPDP 2013, ACM -
    • +Coq: the world's best macro assembler?. PPDP 2013, ACM
  • Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis. -Mtac: A Monad for Typed Tactic Programming in Coq. ICFP 2013 -
    • +Mtac: A Monad for Typed Tactic Programming in Coq. ICFP 2013
  • Aleksandar Nanevski, Viktor Vafeiadis, Josh Berdine. -Structuring the Verification of Heap-Manipulating Programs. POPL 2010 -
    • +Structuring the Verification of Heap-Manipulating Programs. POPL 2010
-
-

Concurrency

-
+
+

Concurrency

+
  • Ilya Sergey, James R. Wilcox, Zachary Tatlock. -Programming and Proving with Distributed Protocols. POPL 2018 -
    • +Programming and Proving with Distributed Protocols. POPL 2018
  • Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee. -Concurrent Data Structures Linked in Time. ECOOP 2017 -
    • +Concurrent Data Structures Linked in Time. ECOOP 2017
  • Mitsuharu Yamamoto, Shogo Sekine, Saki Matsumoto. -Formalization of Karp-Miller Tree Construction on Petri Nets. CPP 2017 -
    • +Formalization of Karp-Miller Tree Construction on Petri Nets. CPP 2017
  • Germán Andrés Delbianco. Hoare-style Reasoning with Higher-order Control: Continuations and Concurrency. -PhD in Computer Science thesis, Universidad Politécnica de Madrid, Spain, July 2017 -
    • +PhD in Computer Science thesis, Universidad Politécnica de Madrid, Spain, July 2017
  • Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco. Hoare-style Specifications as Correctness Conditions for Non-linearizable Concurrent Objects. -OOPSLA 2016 -
    • +OOPSLA 2016
  • Ilya Sergey, Aleksandar Nanevski, Anindya Banerje. -Mechanized Verification of Fine-grained Concurrent Programs. PLDI 2015 -
    • +Mechanized Verification of Fine-grained Concurrent Programs. PLDI 2015
  • Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee. -Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity. ESOP 2015 -
    • +Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity. ESOP 2015
  • Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, Germán Andrés Delbianco. Communicating State Transition Systems for Fine-Grained Concurrent Resources. -ESOP 2014 -
    • +ESOP 2014
  • Ruy Ley-Wild, Aleksandar Nanevski. -Subjective Auxiliary State for Coarse-Grained Concurrency. POPL 2013 -
    • +Subjective Auxiliary State for Coarse-Grained Concurrency. POPL 2013
-
-

Information Flow

-
+
+

Information Flow

+
  • Aleksandar Nanevski, Anindya Banerjee, Deepak Garg. Dependent Type Theory for Verification of Information Flow and Access Control Policies. -ACM Transactions on Programming Languages and Systems (TOPLAS), 35(2):6:1-6:41, 2013 -
    • +ACM Transactions on Programming Languages and Systems (TOPLAS), 35(2):6:1-6:41, 2013
  • Gordon Stewart, Anindya Banerjee, Aleksandar Nanevski. Dependent Types for Enforcement of Information Flow and Erasure Policies in Heterogeneous Data Structures. -PPDP 2013. -
    • +PPDP 2013.
  • Aleksandar Nanevski, Anindya Banerjee, Deepak Garg. Verification of Information Flow and Access Control Policies with Dependent Types. -IEEE Symposium on Security and Privacy (S&P), 2011 -
    • +IEEE Symposium on Security and Privacy (S&P), 2011
-
-

Other Applications

-
+
+

Other Applications

+
    -
  • George Pîrlea, Ilya Sergey. Mechanising Blockchain Consensus. CPP 2018 -
    • +
  • George Pîrlea, Ilya Sergey. Mechanising Blockchain Consensus. CPP 2018
  • Gallego Arias, Emilio Jesús, Olivier Hermant, Pierre Jouvelot. A Taste of Sound Reasoning in Faust. -Thirteenth Linux Audio Conference, paper/code/slides, 2015 -
    • +Thirteenth Linux Audio Conference, paper/code/slides, 2015
  • Maxime Dénès, Benjamin Lesage, Yves Bertot, Adrien Richard. -Formal proof of theorems on genetic regulatory networks. SYNACS 2009, IEEE -
    • +Formal proof of theorems on genetic regulatory networks. SYNACS 2009, IEEE
-
-

Logic, Types, and Verification

-
+
+

Logic, Types, and Verification

+
  • Véronique Benzaken, Evelyne Contejean, Stefania Dumbrava. -Certifying Standard and Stratified Datalog Inference Engines in SSReflect. ITP 2017 -
    • +Certifying Standard and Stratified Datalog Inference Engines in SSReflect. ITP 2017
  • F. Cerqueira, F. Stutz, B. Brandenburg. Prosa: A Case for Readable Mechanized Schedulability Analysis. -Proceedings of the 28th Euromicro Conference on Real-Time Systems (ECRTS 2016) -
    • +Proceedings of the 28th Euromicro Conference on Real-Time Systems (ECRTS 2016)
  • Christian Doczkal, Gert Smolka. -Completeness and Decidability Results for CTL in Coq. ITP 2014 -
    • +Completeness and Decidability Results for CTL in Coq. ITP 2014
  • Christian Doczkal, Gert Smolka. -Constructive Completeness for Modal Logic with Transitive Closure. CPP -
    • +Constructive Completeness for Modal Logic with Transitive Closure. CPP
  • Christian Doczkal, Gert Smolka. -Constructive Formalization of Hybrid Logic with Eventualities. CPP 2011 -
    • +Constructive Formalization of Hybrid Logic with Eventualities. CPP 2011
  • Kasper Svendsen, Lars Birkedal, Aleksandar Nanevski. Partiality, State and Dependent Types. -International Conference on Typed Lambda Calculi and Applications (TLCA) -
    • +International Conference on Typed Lambda Calculi and Applications (TLCA)
-
-

Information theory

-
+
+

Information theory

+
  • Kyosuke Nakano, Manabu Hagiwara. Formalization of binary symmetric erasure channel based on infotheo. -Proceeding of International Symposium on Information Theory and its Application 2016 (ISITA 2016) -
    • +Proceeding of International Symposium on Information Theory and its Application 2016 (ISITA 2016)
  • Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa. Formalization of Reed-Solomon codes and progress report on formalization of LDPC codes. -Proceeding of International Symposium on Information Theory and its Application 2016 (ISITA 2016) -
    • +Proceeding of International Symposium on Information Theory and its Application 2016 (ISITA 2016)
  • Reynald Affeldt, Jacques Garrigue. -Formalization of error-correcting codes: from Hamming to modern coding theory. ITP 2015. -
    • +Formalization of error-correcting codes: from Hamming to modern coding theory. ITP 2015.
  • Ryosuke Obi, Manabu Hagiwara, Reynald Affeldt. Formalization of the variable-length source coding theorem: Direct part. -Proceeding of International Symposium on Information Theory and its Application 2014 (ISITA 2014) -
    • +Proceeding of International Symposium on Information Theory and its Application 2014 (ISITA 2014)
  • Reynald Affeldt, Manabu Hagiwara, Jonas Sénizergues. -Formalization of Shannon's theorems. Journal of Automated Reasoning, 2014 -
    • +Formalization of Shannon's theorems. Journal of Automated Reasoning, 2014
  • Reynald Affeldt, Manabu Hagiwara. -Formalization of Shannon's Theorems in SSReflect-Coq. ITP 2012 -
    • +Formalization of Shannon's Theorems in SSReflect-Coq. ITP 2012
-
-

Tooling about SSReflect and Mathematical Components

-
+
+

Tooling about SSReflect and Mathematical Components

+
  • Jónathan Heras, Ekaterina Komendantskaya. -Proof Pattern Search in Coq/SSReflect. CoRR abs/1402.0081 -
    • +Proof Pattern Search in Coq/SSReflect. CoRR abs/1402.0081
  • Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, Derek Dreyer. -How to make ad hoc proof automation less ad hoc. Journal of Functional Programming -
    • +How to make ad hoc proof automation less ad hoc. Journal of Functional Programming
  • Jónathan Heras, Ekaterina Komendantskaya. -Statistical Proof-Patterns in Coq/SSReflect. CoRR abs/1301.6039 -
    • +Statistical Proof-Patterns in Coq/SSReflect. CoRR abs/1301.6039
  • Vladimir Komendantsky, Alexander Konovalov, Steve Linton. -Interfacing Coq + SSReflect with GAP. Electr. Notes Theor. Comput. Sci. 285 -
    • +Interfacing Coq + SSReflect with GAP. Electr. Notes Theor. Comput. Sci. 285
  • Iain Whiteside, David Aspinall, Gudmund Grov. -An Essence of SSReflect. AISC/MKM/Calculemus -
    • +An Essence of SSReflect. AISC/MKM/Calculemus
  • Georges Gonthier, Enrico Tassi. -A Language of Patterns for Subterm Selection. ITP 2012 -
    • +A Language of Patterns for Subterm Selection. ITP 2012
  • Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, Derek Dreyer. -How to Make Ad Hoc Proof Automation Less Ad Hoc. ICFP 2011 -
    • +How to Make Ad Hoc Proof Automation Less Ad Hoc. ICFP 2011
  • Georges Gonthier, Assia Mahboubi. -An introduction to small scale reflection in Coq, Journal of Formalized Reasoning -
    • +An introduction to small scale reflection in Coq, Journal of Formalized Reasoning
  • François Garillot, Georges Gonthier, Assia Mahboubi, Laurence Rideau. -Packaging Mathematical Structures. TPHOLs 2019 -
    • +Packaging Mathematical Structures. TPHOLs 2019
diff --git a/papers.org b/papers.org index 2815d9a2..c065d5cf 100644 --- a/papers.org +++ b/papers.org @@ -27,8 +27,8 @@ wiki]]. * Mathematics -- Florent Bréhard, Assia Mahboubi and Damien Pous. A certificate-based - approach to formally verified approximations. ITP 2019. [[https://hal-cstb.archives-ouvertes.fr/LAAS-MAC/hal-02088529v1][pdf]] +- Florent Bréhard, Assia Mahboubi and Damien Pous. _A certificate-based + approach to formally verified approximations_. ITP 2019. [[https://hal-cstb.archives-ouvertes.fr/LAAS-MAC/hal-02088529v1][pdf]] - Xavier Allamigeon, Ricardo D. Katz. _A formalization of convex polyhedra based on the simplex method_. ITP 2017 - Evmorfia-Iro Bartzia. @@ -84,6 +84,9 @@ wiki]]. * Programming and Algorithms +- Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, Kazunari Tanaka. + _Proving tree algorithms for succinct data structures_. + ITP 2019, [[https://arxiv.org/pdf/1904.02809.pdf][pdf]] - Cyril Cohen, Damien Rouhling. _A refinement-based approach to large scale reflection for algebra_. JFLA 2017 - Timmy Weerwag.