EN FR
EN FR


previous Previous | up Home


Bibliography

Publications of the year

Articles in International Peer-Reviewed Journals

  • 1B. Ahrens, A. Hirschowitz, A. Lafont, M. Maggesi.

    Reduction Monads and Their Signatures, in: Proceedings of the ACM on Programming Languages, January 2020. [ DOI : 10.1145/3371099 ]

    https://hal.inria.fr/hal-02380682
  • 2Z. CHENG, M. Tisi, R. Douence.

    CoqTL: A Coq DSL for Rule-Based Model Transformation, in: Software and Systems Modeling, 2019, pp. 1-15, forthcoming. [ DOI : 10.1007/s10270-019-00765-6 ]

    https://hal.archives-ouvertes.fr/hal-02333564
  • 3G. Gilbert, J. Cockx, M. Sozeau, N. Tabareau.

    Definitional Proof-Irrelevance without K, in: Proceedings of the ACM on Programming Languages, January 2019, pp. 1-28. [ DOI : 10.1145/329031610.1145/3290316 ]

    https://hal.inria.fr/hal-01859964
  • 4G. Jaber.

    SyTeCi: Automating Contextual Equivalence for Higher-Order Programs with References, in: Proceedings of the ACM on Programming Languages, 2019, vol. 28, pp. 1-28, forthcoming. [ DOI : 10.1145/3371127 ]

    https://hal.archives-ouvertes.fr/hal-02388621
  • 5A. Mahboubi, G. Melquiond, T. Sibut-Pinote.

    Formally Verified Approximations of Definite Integrals, in: Journal of Automated Reasoning, February 2019, vol. 62, no 2, pp. 281-300. [ DOI : 10.1007/s10817-018-9463-7 ]

    https://hal.inria.fr/hal-01630143
  • 6P.-M. Pédrot, N. Tabareau, H. J. Fehrmann, É. Tanter.

    A Reasonably Exceptional Type Theory, in: Proceedings of the ACM on Programming Languages, August 2019, vol. 3, pp. 1-29. [ DOI : 10.1145/3341712 ]

    https://hal.inria.fr/hal-02189128
  • 7P.-M. Pédrot, N. Tabareau.

    The Fire Triangle : How to Mix Substitution, Dependent Elimination, and Effects, in: Proceedings of the ACM on Programming Languages, January 2020. [ DOI : 10.1145/3371126 ]

    https://hal.archives-ouvertes.fr/hal-02383109
  • 8M. Sozeau, S. Boulier, Y. Forster, N. Tabareau, T. Winterhalter.

    Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq, in: Proceedings of the ACM on Programming Languages, January 2020. [ DOI : 10.1145/3371076 ]

    https://hal.archives-ouvertes.fr/hal-02380196
  • 9N. Tabareau, É. Tanter.

    Chemical foundations of distributed aspects, in: Distributed Computing, June 2019, vol. 32, no Issue 3, pp. 193–216, forthcoming. [ DOI : 10.1007/s00446-018-0334-6 ]

    https://hal.inria.fr/hal-01811884

International Conferences with Proceedings

  • 10B. Ahrens, A. Hirschowitz, A. Lafont, M. Maggesi.

    Modular specification of monads through higher-order presentations, in: FSCD 2019 - 4th International Conference on Formal Structures for Computation and Deduction, Dortmund, Germany, June 2019, pp. 1-16, https://arxiv.org/abs/1903.00922 - 17 pages. [ DOI : 10.4230/LIPIcs.FSCD.2019.6 ]

    https://hal.archives-ouvertes.fr/hal-02307998
  • 11T. Altenkirch, S. Boulier, A. Kaposi, N. Tabareau.

    Setoid type theory - a syntactic translation, in: MPC 2019 - 13th International Conference on Mathematics of Program Construction, Porto, Portugal, LNCS, Springer, October 2019, vol. 11825, pp. 155-196. [ DOI : 10.1007/978-3-030-33636-3_7 ]

    https://hal.inria.fr/hal-02281225
  • 12F. Bréhard, A. Mahboubi, D. Pous.

    A certificate-based approach to formally verified approximations, in: ITP 2019 - Tenth International Conference on Interactive Theorem Proving, Portland, United States, 2019, pp. 1-19. [ DOI : 10.4230/LIPIcs.ITP.2019.8 ]

    https://hal.laas.fr/hal-02088529
  • 13É. Miquey.

    Revisiting the duality of computation: an algebraic analysis of classical realizability models, in: CSL 2020, Barcelone, Spain, LIPIcs, CSL 2020, January 2020, vol. 152, https://arxiv.org/abs/1910.02732.

    https://hal.archives-ouvertes.fr/hal-02305560
  • 14A. Mörtberg, L. Pujet.

    Cubical Synthetic Homotopy Theory, in: CPP 2020 - 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, New Orleans, United States, ACM, January 2020. [ DOI : 10.1145/3372885.3373825 ]

    https://hal.archives-ouvertes.fr/hal-02394145
  • 15T. Winterhalter, M. Sozeau, N. Tabareau.

    Eliminating Reflection from Type Theory : To the Legacy of Martin Hofmann, in: CPP 2019 - 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Lisbonne, Portugal, ACM, January 2019, pp. 91-103. [ DOI : 10.1145/3293880.3294095 ]

    https://hal.archives-ouvertes.fr/hal-01849166

Conferences without Proceedings

  • 16C. Chenavier, M. Lucas.

    The Diamond Lemma for non-terminating rewriting systems using deterministic reduction strategies, in: IWC 2019 - 8th International Workshop on Confluence, Dortmund, Germany, June 2019, pp. 1-5.

    https://hal.archives-ouvertes.fr/hal-02385139
  • 17G. Munch-Maccagnoni, R. Douence.

    Efficient Deconstruction with Typed Pointer Reversal (abstract), in: ML 2019 - Workshop, Berlin, Germany, KC Sivaramakrishnan, 2019, pp. 1-8.

    https://hal.inria.fr/hal-02177326

Internal Reports

  • 18I. Zhirkov, J. Cohen, R. Douence.

    Memory bijections: reasoning about exact memory transformations induced by refactorings in CompCert C, LS2N, Université de Nantes, March 2019.

    https://hal.archives-ouvertes.fr/hal-02078356

Other Publications

References in notes
  • 27A. Abel, T. Coquand.

    Untyped Algorithmic Equality for Martin-Löf’s Logical Framework with Surjective Pairs, in: Typed Lambda Calculi and Applications, P. Urzyczyn (editor), Lecture Notes in Computer Science, Springer Berlin Heidelberg, 2005, vol. 3461, pp. 23-38.

    http://dx.doi.org/10.1007/11417170_4
  • 28B. Accattoli, G. Guerrieri.

    Open Call-by-Value, in: Programming Languages and Systems, January 2016.

    http://dx.doi.org/10.1007/978-3-319-47958-3_12
  • 29D. Ahman, N. Ghani, G. D. Plotkin.

    Dependent Types and Fibred Computational Effects, in: Proc. FoSSaCS, 2015.
  • 30A. Ajouli, J. Cohen, J.-C. Royer.

    Transformations between Composite and Visitor Implementations in Java, in: Software Engineering and Advanced Applications (SEAA), 2013 39th EUROMICRO Conference on, Sept 2013, pp. 25–32.

    http://dx.doi.org/10.1109/SEAA.2013.53
  • 31J. Aldrich.

    The power of interoperability: why objects are inevitable, in: ACM Symposium on New Ideas in Programming and Reflections on Software, Onward! 2013, part of SPLASH '13, Indianapolis, IN, USA, October 26-31, 2013, A. L. Hosking, P. T. Eugster, R. Hirschfeld (editors), ACM, 2013, pp. 101–116.
  • 32T. Altenkirch, C. McBride, W. Swierstra.

    Observational equality, now!, in: Proceedings of the ACM Workshop on Programming Languages meets Program Verification (PLPV 2007), Freiburg, Germany, October 2007, pp. 57–68.
  • 33J.-M. Andreoli.

    Logic Programming with Focusing Proof in Linear Logic, in: Journal of Logic and Computation, 1992, vol. 2, no 3, pp. 297-347.
  • 34E. Arafailova, N. Beldiceanu, R. Douence, M. Carlsson, P. Flener, M. A. F. Rodríguez, J. Pearson, H. Simonis.

    Global Constraint Catalog, Volume II, Time-Series Constraints, in: CoRR, 2016, vol. abs/1609.08925.

    http://arxiv.org/abs/1609.08925
  • 35E. Arafailova, N. Beldiceanu, R. Douence, P. Flener, M. A. F. Rodríguez, J. Pearson, H. Simonis.

    Time-Series Constraints: Improvements and Application in CP and MIP Contexts, in: Integration of AI and OR Techniques in Constraint Programming - 13th International Conference, CPAIOR 2016, Banff, AB, Canada, May 29 - June 1, 2016, Proceedings, C. Quimper (editor), Lecture Notes in Computer Science, Springer, 2016, vol. 9676, pp. 18–34.

    https://doi.org/10.1007/978-3-319-33954-2_2
  • 36A. F. Barco, J. Fages, É. Vareilles, M. Aldanondo, P. Gaborit.

    Open Packing for Facade-Layout Synthesis Under a General Purpose Solver, in: Principles and Practice of Constraint Programming - 21st International Conference, CP 2015, Cork, Ireland, August 31 - September 4, 2015, Proceedings, G. Pesant (editor), Lecture Notes in Computer Science, Springer, 2015, vol. 9255, pp. 508–523.

    http://dx.doi.org/10.1007/978-3-319-23219-5_36
  • 37N. Beldiceanu, M. Carlsson, R. Douence, H. Simonis.

    Using finite transducers for describing and synthesising structural time-series constraints, in: Constraints, 2016, vol. 21, no 1, pp. 22–40.

    http://dx.doi.org/10.1007/s10601-015-9200-3
  • 38S. Berardi, M. Bezem, T. Coquand.

    On the computational content of the axiom of choice, in: The Journal of Symbolic Logic, 1998, vol. 63, no 02, pp. 600–622.
  • 39M. Bezem, T. Coquand, S. Huber.

    A model of type theory in cubical sets, in: Preprint, September, 2013.
  • 40S. Boulier, P.-M. Pédrot, N. Tabareau.

    The next 700 syntactical models of type theory, in: Certified Programs and Proofs (CPP 2017), Paris, France, January 2017, pp. 182 - 194. [ DOI : 10.1145/3018610.3018620 ]

    https://hal.inria.fr/hal-01445835
  • 41E. Brady.

    Idris, a general-purpose dependently typed programming language: Design and implementation, in: J. Funct. Program., 2013, vol. 23, no 5, pp. 552–593.

    https://doi.org/10.1017/S095679681300018X
  • 42F. Chyzak, A. Mahboubi, T. Sibut-Pinote, E. Tassi.

    A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3), in: Interactive Theorem Proving, R. G. Gerwin Klein (editor), Lecture Notes in Computer Science, Springer, 2014, vol. 8558.
  • 43J. Cohen, A. Ajouli.

    Practical Use of Static Composition of Refactoring Operations, in: Proceedings of the 28th Annual ACM Symposium on Applied Computing, SAC '13, ACM, 2013, pp. 1700–1705.

    http://dx.doi.org/10.1145/2480362.2480684
  • 44J. Cohen.

    Renaming Global Variables in C Mechanically Proved Correct, in: Proceedings of the Fourth International Workshop on Verification and Program Transformation, Eindhoven, The Netherlands, 2nd April 2016, G. Hamilton, A. Lisitsa, A. P. Nemytykh (editors), Electronic Proceedings in Theoretical Computer Science, Open Publishing Association, 2016, vol. 216, pp. 50-64.

    http://dx.doi.org/10.4204/EPTCS.216.3
  • 45C. Cohen, T. Coquand, S. Huber, A. Mörtberg.

    Cubical Type Theory: a constructive interpretation of the univalence axiom, 2016, To appear in post-proceedings of Types for Proofs and Programs (TYPES 2015).
  • 46P. Cohen, M. Davis.

    Set theory and the continuum hypothesis, WA Benjamin New York, 1966.
  • 47J. Cohen, R. Douence, A. Ajouli.

    Invertible Program Restructurings for Continuing Modular Maintenance, in: Software Maintenance and Reengineering (CSMR), 2012 16th European Conference on, March 2012, pp. 347-352.

    http://dx.doi.org/10.1109/CSMR.2012.42
  • 48W. R. Cook.

    On understanding data abstraction, revisited, in: Proceedings of the 24th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2009, October 25-29, 2009, Orlando, Florida, USA, S. Arora, G. T. Leavens (editors), ACM, 2009, pp. 557–572.

    http://doi.acm.org/10.1145/1640089.1640133
  • 49Coq Development Team, The.

    The Coq proof assistant reference manual, 2015, Version 8.5.

    http://coq.inria.fr
  • 50P.-L. Curien, M. Fiore, G. Munch-Maccagnoni.

    A Theory of Effects and Resources: Adjunction Models and Polarised Calculi, in: Proc. POPL, 2016.

    http://dx.doi.org/10.1145/2837614.2837652
  • 51P.-L. Curien, H. Herbelin.

    The duality of computation, in: ACM SIGPLAN Notices, 2000, vol. 35, pp. 233–243.
  • 52D. Delahaye, M. Mayero.

    Dealing with algebraic expressions over a field in Coq using Maple, in: J. Symbolic Comput., 2005, vol. 39, no 5, pp. 569–592, Special issue on the integration of automated reasoning and computer algebra systems.

    http://dx.doi.org/10.1016/j.jsc.2004.12.004
  • 53R. Douence, X. Lorca, N. Loriant.

    Lazy Composition of Representations in Java, in: Software Composition, 8th International Conference, SC 2009, Zurich, Switzerland, July 2-3, 2009. Proceedings, A. Bergel, J. Fabry (editors), Lecture Notes in Computer Science, Springer, 2009, vol. 5634, pp. 55–71.

    https://doi.org/10.1007/978-3-642-02655-3_6
  • 54T. Ehrhard.

    Call-by-push-value from a linear logic point of view, in: European Symposium on Programming Languages and Systems, Springer, 2016, pp. 202–228.
  • 55A. Frisch, G. Castagna, V. Benzaken.

    Semantic Subtyping: Dealing Set-theoretically with Function, Union, Intersection, and Negation Types, in: J. ACM, September 2008, vol. 55, no 4, pp. 19:1–19:64.
  • 56C. Führmann.

    Direct Models for the Computational Lambda Calculus, in: Electr. Notes Theor. Comput. Sci., 1999, vol. 20, pp. 245-292.
  • 57J.-Y. Girard.

    Linear Logic, in: Theoretical Computer Science, 1987, vol. 50, pp. 1-102.
  • 58J.-Y. Girard, A. Scedrov, P. J. Scott.

    Normal Forms and Cut-Free Proofs as Natural Transformations, in: in : Logic From Computer Science, Mathematical Science Research Institute Publications 21, Springer-Verlag, 1992, pp. 217–241.
  • 59G. Gonthier, A. Asperti, J. Avigad, Y. Bertot, C. Cohen, F. Garillot, S. Roux, A. Mahboubi, R. O’Connor, S. Ould Biha, I. Pasca, L. Rideau, A. Solovyev, E. Tassi, L. Théry.

    A Machine-Checked Proof of the Odd Order Theorem, in: Interactive Theorem Proving, S. Blazy, C. Paulin-Mohring, D. Pichardie (editors), Lecture Notes in Computer Science, Springer Berlin Heidelberg, 2013, vol. 7998, pp. 163-179.

    http://dx.doi.org/10.1007/978-3-642-39634-2_14
  • 60G. Gonthier.

    Formal proofs—the four-colour theorem, in: Notices of the AMS, 2008, vol. 55, no 11, pp. 1382-1393.
  • 61G. Gonthier, A. Mahboubi, E. Tassi.

    A Small Scale Reflection Extension for the Coq system, Inria, 2008, no RR-6455, The Reference Manual of the Ssreflect extension to the Coq tactic language, available at http://hal.inria.fr/inria-00258384.
  • 62T. G. Griffin.

    A Formulae-as-Types Notion of Control, in: Seventeenth Annual ACM Symposium on Principles of Programming Languages, ACM Press, 1990, pp. 47–58.
  • 63Y. Guéhéneuc, R. Douence, N. Jussien.

    No Java without Caffeine: A Tool for Dynamic Analysis of Java Programs, in: 17th IEEE International Conference on Automated Software Engineering (ASE 2002), 23-27 September 2002, Edinburgh, Scotland, UK, IEEE Computer Society, 2002, 117 p.

    https://doi.org/10.1109/ASE.2002.1115000
  • 64T. C. Hales, M. Adams, G. Bauer, D. T. Dang, J. Harrison, T. L. Hoang, C. Kaliszyk, V. Magron, S. McLaughlin, T. T. Nguyen, T. Q. Nguyen, T. Nipkow, S. Obua, J. Pleso, J. Rute, A. Solovyev, A. H. T. Ta, T. N. Tran, D. T. Trieu, J. Urban, K. K. Vu, R. Zumkeller.

    A formal proof of the Kepler conjecture, in: CoRR, 2015, vol. abs/1501.02155.

    http://arxiv.org/abs/1501.02155
  • 65H. A. Helfgott.

    The ternary Goldbach conjecture is true, in: ArXiv e-prints, December 2013.
  • 66H. Herbelin.

    A Constructive Proof of Dependent Choice, Compatible with Classical Logic, in: LICS 2012 - 27th Annual ACM/IEEE Symposium on Logic in Computer Science, Dubrovnik, Croatia, IEEE Computer Society, June 2012, pp. 365-374.

    https://hal.inria.fr/hal-00697240
  • 67H. Herbelin, É. Miquey.

    Toward dependent choice: a classical sequent calculus with dependent types, in: TYPES 2015, 2015.
  • 68T. Hirschowitz.

    Cartesian closed 2-categories and permutation equivalence in higher-order rewriting, in: Logical Methods in Computer Science, 2013, vol. 9, no 3, 10 p, 19 pages. [ DOI : 10.2168/LMCS-9(3:10)2013 ]

    https://hal.archives-ouvertes.fr/hal-00540205
  • 69F. Immler.

    Verified Reachability Analysis of Continuous Systems, in: Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, C. Baier, C. Tinelli (editors), Lecture Notes in Computer Science, Springer, 2015, vol. 9035, pp. 37–51.
  • 70G. Jaber, G. Lewertowski, P.-M. Pédrot, M. Sozeau, N. Tabareau.

    The Definitional Side of the Forcing, in: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016, 2016, pp. 367–376.
  • 71G. Jaber, N. Tabareau, M. Sozeau.

    Extending type theory with forcing, in: Logic in Computer Science (LICS), 2012, IEEE, 2012, pp. 395–404.
  • 72C. B. Jay, N. Ghani.

    The Virtues of Eta-Expansion, in: J. Funct. Program., 1995, vol. 5, no 2, pp. 135-154.
  • 73U. Kohlenbach.

    Applied proof theory: proof interpretations and their use in mathematics, Springer Science & Business Media, 2008.
  • 74J.-L. Krivine.

    Realizability algebras II : new models of ZF + DC, in: Logical Methods in Computer Science, 2012, vol. 8, no 1.
  • 75J. Lambek, P. J. Scott.

    Introduction to higher order categorical logic, Cambridge University Press, New York, NY, USA, 1986.
  • 76S. M. Lane, I. Moerdijk.

    Sheaves in Geometry and Logic, Springer-Verlag, 1992.
  • 77R. Lepigre.

    A classical realizability model for a semantical value restriction, in: European Symposium on Programming Languages and Systems, Springer, 2016, pp. 476–502.
  • 78X. Leroy.

    Formal certification of a compiler back-end or: programming a compiler with a proof assistant, in: ACM SIGPLAN Notices, 2006, vol. 41, no 1, pp. 42–54.
  • 79P. B. Levy.

    Call-By-Push-Value: A Functional/Imperative Synthesis, Semantic Structures in Computation, Springer, 2004, vol. 2.
  • 80P. B. Levy.

    Contextual isomorphisms, in: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, ACM, 2017, pp. 400–414.
  • 81C. Liang, D. Miller.

    Focusing and polarization in linear, intuitionistic, and classical logics, in: Theor. Comput. Sci., 2009, vol. 410, no 46, pp. 4747-4768.
  • 82Z. Luo, S. Soloviev, T. Xue.

    Coercive subtyping: Theory and implementation, in: Inf. Comput., 2013, vol. 223, pp. 18–42.
  • 83J. Lurie.

    Higher topos theory, Annals of mathematics studies, Princeton University Press, Princeton, N.J., Oxford, 2009.
  • 84S. Mac Lane.

    Natural associativity and commutativity, in: Selected Papers, 1979, pp. 415–433.
  • 85P. Martin-Löf.

    An intuitionistic theory of types: predicative part, in: Logic Colloquium '73, 1975, vol. Studies in Logic and the Foundations of Mathematics, no 80, pp. 73–118.
  • 86P.-A. Melliès.

    Asynchronous Games 3 An Innocent Model of Linear Logic, in: Electr. Notes Theor. Comput. Sci., 2005, vol. 122, pp. 171-192.
  • 87P.-A. Melliès.

    Asynchronous Games 4: A Fully Complete Model of Propositional Linear Logic, in: LICS, 2005, pp. 386-395.
  • 88P.-A. Melliès, N. Tabareau.

    Resource modalities in tensor logic, in: Ann. Pure Appl. Logic, 2010, vol. 161, no 5, pp. 632-653.
  • 89É. Miquey.

    A classical sequent calculus with dependent types, in: European Symposium on Programming, Springer, 2017, pp. 777–803.
  • 90E. Moggi.

    Computational lambda-calculus and monads, in: Proceedings of the Fourth Annual IEEE Symposium on Logic in Computer Science (LICS 1989), IEEE Computer Society Press, June 1989, pp. 14–23.
  • 91E. Moggi.

    Notions of computation and monads, in: Inf. Comput., July 1991, vol. 93, no 1, pp. 55–92.

    http://dx.doi.org/10.1016/0890-5401(91)90052-4
  • 92G. Munch-Maccagnoni.

    Formulae-as-Types for an Involutive Negation, in: Proceedings of the joint meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (CSL-LICS), 2014.
  • 93G. Munch-Maccagnoni.

    Models of a Non-Associative Composition, in: Proc. FoSSaCS, A. Muscholl (editor), LNCS, Springer, 2014, vol. 8412, pp. 397–412.
  • 94G. Munch-Maccagnoni.

    Note on Curry's style for Linear Call-by-Push-Value, 2017.

    https://hal.inria.fr/hal-01528857
  • 95A. Nanevski, G. Morrisett, A. Shinnar, P. Govereau, L. Birkedal.

    Ynot: Reasoning with the awkward squad, 2008.
  • 96C. Okasaki.

    Purely functional data structures, Cambridge University Press, 1999.
  • 97C. Prud'homme, X. Lorca, R. Douence, N. Jussien.

    Propagation engine prototyping with a domain specific language, in: Constraints, 2014, vol. 19, no 1, pp. 57–76.

    https://doi.org/10.1007/s10601-013-9151-5
  • 98C. Prud'homme.

    Contrôle de la propagation et de la recherche dans un solveur de contraintes. (Controlling propagation and search within a constraint solver), École des mines de Nantes, France, 2014.

    https://tel.archives-ouvertes.fr/tel-01060921
  • 99P.-M. Pédrot, N. Tabareau.

    An Effectful Way to Eliminate Addiction to Dependence, January 2017.

    https://hal.inria.fr/hal-01441829
  • 100K. Quirin, N. Tabareau.

    Lawvere-Tierney sheafification in Homotopy Type Theory, in: Journal of Formalized Reasoning, 2016, vol. 9, no 2. [ DOI : 10.6092/issn.1972-5787/6232 ]

    https://hal.inria.fr/hal-01451710
  • 101J. C. Reynolds.

    Types, Abstraction and Parametric Polymorphism, in: IFIP Congress, 1983, pp. 513-523.
  • 102P. Selinger.

    Control Categories and Duality: On the Categorical Semantics of the Lambda-Mu Calculus, in: Math. Struct in Comp. Sci., 2001, vol. 11, no 2, pp. 207–260.
  • 103S. G. Simpson.

    Subsystems of Second Order Arithmetic, Second, Cambridge University Press, 2009, Cambridge Books Online.

    http://dx.doi.org/10.1017/CBO9780511581007
  • 104K. Støvring.

    Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative, in: Logical Methods in Computer Science, 2006, vol. 2, no 2.
  • 105N. Swamy, C. Hriţcu, C. Keller, A. Rastogi, A. Delignat-Lavaud, S. Forest, K. Bhargavan, C. Fournet, P.-Y. Strub, M. Kohlweiss, J.-K. Zinzindohoue, S. Zanella-Béguelin.

    Dependent Types and Multi-Monadic Effects in F*, in: 43nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), ACM, January 2016, pp. 256-270.

    https://www.fstar-lang.org/papers/mumon/
  • 106É. Tanter, N. Tabareau.

    Gradual Certified Programming in Coq, in: Proceedings of the 11th ACM Dynamic Languages Symposium (DLS 2015), Pittsburgh, PA, USA, ACM Press, October 2015, pp. 26–40.
  • 107Univalent Foundations Project.

    Homotopy Type Theory: Univalent Foundations for Mathematics, http://homotopytypetheory.org/book, 2013.
  • 108M. Vákár.

    A Framework for Dependent Types and Effects, in: arXiv preprint arXiv:1512.08009, 2015.
  • 109B. Ziliani, D. Dreyer, N. R. Krishnaswami, A. Nanevski, V. Vafeiadis.

    Mtac: A monad for typed tactic programming in Coq, in: Journal of Functional Programming, 2015, vol. 25.

    http://dx.doi.org/10.1017/S0956796815000118
  • 110F. van Raamsdonk.

    Higher-order Rewriting, in: Proc. Rewrit. Tech. App., LNCS, Springer, 1999, vol. 1631, pp. 220-239.


previous Previous | up Home