print · login   

If there are any publications you would like to see added to this page, please send them by e-mail to pubs.eutypes@cs.ru.nl. The .bib file can be found here.

Proceedings of Types Conferences

Publications by EUTYPES Members

2016

  • Negri, S. & von Plato, J. (2002). Hilbert's Last Problem. Philosophical Transactions of the Royal Society.
  • Craciun, F. & Glodean, G. (2010). Towards Compiling Region Types into RTSJ-compliant Java Code. In Symbolic and Numeric Algorithms for Scientific ComputingSYNASC.
  • Ahrens, B. & Matthes, R. (2015). Heterogeneous Substitution Systems Revisited. In 21st International Conference on Types for Proofs and Programs, TYPES 2015, May 18-21, 2015, Tallinn, Estonia (pp. 2:1--2:23).
  • Bezem, M., Coquand, T., & Parmann, E. (2015). Non-Constructivity in Kan Simplicial Sets. In 13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015, July 1-3, 2015, Warsaw, Poland (pp. 92--106).
  • von Plato, J. (2015). In search of the roots of formal computation. In International Conference on the History and Philosophy of Computing (pp. 300--320).
  • Abel, A. (2016). Compositional Coinduction with Sized Types. In Coalgebraic Methods in Computer Science, 13th IFIP WG 1.3 International Workshop, CMCS 2016, Colocated with ETAPS 2016, Eindhoven, The Netherlands, April 2-3, 2016, Revised Selected Papers (pp. 5--10).
  • Abel, A. & Pientka, B. (2016). Well-founded recursion with copatterns and sized types. Journal of Functional Programming, 26, 61.
  • Abel, A. & Winterhalter, T. (2016). An Extension of Martin-Löf Type Theory with Sized Types. In 22nd International Conference on Types for Proofs and Programs, TYPES 2016, Novi Sad, Serbia, May 23-26, 2016, Book of Abstracts. EasyChair.
  • Abel, A. & Chapman, J. (2016). Normalization by Evaluation in the Delay Monad. In 22nd International Conference on Types for Proofs and Programs, TYPES 2016, Novi Sad, Serbia, May 23-26, 2016, Book of Abstracts. EasyChair.
  • Abel, A., Coquand, T., & Mannaa, B. (2016). On Decidability of Conversion in Type Theory. In 22nd International Conference on Types for Proofs and Programs, TYPES 2016, Novi Sad, Serbia, May 23-26, 2016, Book of Abstracts. EasyChair.
  • Adams, R., Bezem, M., & Coquand, T. (2016). A Normalizing Computation Rule for Propositional Extensionality in Higher-Order Minimal Logic. In 22nd International Conference on Types for Proofs and Programs, TYPES 2016, May 23-26, 2016, Novi Sad, Serbia (pp. 3:1--3:20).
  • Reynald Affeldt and Cyril Cohen. Formal Foundations of 3D Geometry to Model Robot Manipulators. In Conference on Certified Programs and Proofs 2017, Paris, France, January 2017
  • D. Ahman, N. Ghani, G. Plotkin. Dependent types and fibred computational effects. In B. Jacobs, C. Löding, eds., Proc. of 19th Int. Conf. on Foundations of Software Science and Computation Structures, FoSSaCS 2016 (Eindhoven, April 2016), v. 9634 of Lect. Notes in Comput. Sci., pp. 36-54. Springer, 2016.
  • D. Ahman, T. Uustalu. Directed containers as categories. In R. Atkey, N. Krishnaswami, eds., Proc. of 6th Wksh. on Mathematically Structured Functional Programming, MSFP 2016 (Eindhoven, April 2016), v. 207 of Electron. Proc. in Theor. Comput. Sci., pp. 89-98. Open Publishing Assoc., 2016.
  • Altenkirch, T., Capriotti, P. and Kraus, N. (2016). Extending homotopy type theory with strict equality. 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). DOI:10.4230/LIPIcs.CSL.2016.21
  • Altenkirch, T. & Kaposi, A. (2016). Normalisation by Evaluation for Dependent Types. In 22nd International Conference on Types for Proofs and Programs, TYPES 2016. University of Novi Sad.
  • Altenkirch, T. & Kaposi, A. (2016). Normalisation by Evaluation for Dependent Types. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), Dagstuhl, Germany, 2016 (pp. 6:1--6:16). Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik.
  • Arrighi, P. & Dowek, G. (2016). Free fall and cellular automata. Electronic Proceedings in Theoretical Computer Science, 204, 1 - 10. https://hal.inria.fr/hal-01421712
  • Arrighi, P., Martiel, S., & Perdrix, S. (2016). Reversible Causal Graph Dynamics. In Reversible Computation, Bologna, Italy, 2016 (pp. 73-88).
  • Assaf, A., Dowek, G., Jouannaud, J.-P., & Liu, J. (2016). Encoding Proofs in Dedukti: the case of Coq proofs. In Proceedings Hammers for Type Theories, Coimbra, Portugal, 2016. Easy Chair.
  • Assaf, A., Dowek, G., Jouannaud, J.-P., & Liu, J. (2016). Untyped Confluence in Dependent Type Theories. In Proceedings Higher-Order Rewriting Workshop, Porto, Portugal, 2016. Easy-Chair.
  • Assaf, A., Burel, G., Cauderlier, R., Delahaye, D., Dowek, G., Dubois, C., Gilbert, F., Halmagrand, P., Hermant, O., & Saillard, R. (2016). Expressing theories in the λΠ-calculus modulo theory and in the Dedukti system. In TYPES: Types for Proofs and Programs, Novi SAd, Serbia, 2016.
  • Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub, and Rébecca Zucchini. Strong Non-Interference and Type-Directed Higher-Order Masking. In CCS 2016 - 23rd ACM Conference on Computer and Communications Security, pages 116 – 129, Vienna, Austria, October 2016. ACM.
  • Gilles Barthe, No ́emie Fong, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. Advanced Probabilistic Couplings for Differential Privacy. In 23rd ACM Conference on Computer and Communications Security, pages 55 – 67, Vienna, Austria, October 2016.
  • Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. A program logic for union bounds. In The 43rd International Colloquium on Automata, Languages and Programming, Rome, Italy, July 2016
  • Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. Proving Differential Privacy via Probabilistic Couplings. In Thirty-First Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 749 – 758, New York, United States, July 2016
  • Sophie Bernard, Yves Bertot, Laurence Rideau, and Pierre-Yves Strub. Formal Proofs of Transcendence for e and π as an Application of Multivariate and Symmetric Polynomials. In Jeremy Avigad and Adam Chlipala, editors, Certified Programs and Proofs, page 12, St Petersburg, Florida, United States, January 2016. ACM Press
  • Bezem, M., Coquand, T., Nakata, K., & Parmann, E. (2016). Realizability at Work: Separating Two Constructive Notions of Finiteness. In 22nd International Conference on Types for Proofs and Programs, TYPES 2016, May 23-26, 2016, Novi Sad, Serbia (pp. 6:1--6:23).
  • Birkedal, L., Jaber, G., Sieczkowski, F., & Thamsborg, J. (2016). A Kripke Logical Relation for Effect-Based Program Transformations. Information and Computation.
  • Bizjak, A., Grathwohl, H. B., Clouston, R., Møgelberg, R. E., & Birkedal, L. (2016). Guarded Dependent Type Theory with Coinductive Types. In Proceedings of FOSSACS 2016.
  • Blot, V. (2016). Hybrid realizability for intuitionistic and classical choice. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016 (pp. 575--584).
  • Blot, V. (2016). Classical Extraction in Continuation Models. In 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, June 22-26, 2016, Porto, Portugal (pp. 13:1--13:17).
  • Booij, A. B., Escardó, M. H., Lumsdaine, P. L., & Shulman, M. (2016). Parametricity, Automorphisms of the Universe, and Excluded Middle. In 22nd International Conference on Types for Proofs and Programs, TYPES 2016, May 23-26, 2016, Novi Sad, Serbia (pp. 7:1--7:14).
  • Guillaume Cano, Cyril Cohen, Maxime Dénès, Anders Mörtberg, and Vincent Siles. Formalized Linear Algebra over Elementary Divisor Rings in Coq. Logical Methods in Computer Science, June 2016.
  • V. Capretta, T. Uustalu. A coalgebraic view of bar recursion and bar induction. In B. Jacobs, C. Löding, eds., Proc. of 19th Int. Conf. on Foundations of Software Science and Computation Structures, FoSSaCS 2016 (Eindhoven, April 2016), v. 9634 of Lect. Notes in Comput. Sci., pp. 91-106. Springer, 2016.
  • Cauderlier, R. & Dubois, C. (2016). ML Pattern-Matching, Recursion, and Rewriting: From FoCaLiZe to Dedukti. In ICTAC 2016 - 13th International Colloquium on Theoretical Aspects of Computing, Taipei, Taiwan, 2016 (pp. 459-468).
  • Cauderlier, R. (2016). A Rewrite System for Proof Constructivization. In Workshop on Logical Frameworks and Meta-Languages: Theory and Practice 2016, Porto, Portugal, 2016 (pp. 1 - 7).
  • Chatzikyriakidis, S. & Luo, Z. (2016). Proof Assistants for Natural Language Semantics. LACL 2016. Nancy.
  • Ciobâca, S., Lucanu, D., Rusu, V., & Rosu, G. (2016). A language-independent proof system for full program equivalence. Formal Asp. Comput., 28(3), 469--497. https://doi.org/10.1007/s00165-016-0361-7
  • Cyril Cohen and Boris Djalal. Formalization of a Newton Series Representation of Polynomials. In Jeremy Avigad and Adam Chlipala, editors, Certified Programs and Proofs, St. Petersburg, Florida, United States, January 2016.
  • Clouston, R., Bizjak, A., Grathwohl, H. B., & Birkedal, L. (2016). The Guarded Lambda Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types. Logical Methods in Computer Science.
  • Cockx, J. & Abel, A. (2016). Sprinkles of Extensionality for Your Vanilla Type Theory. In 22nd International Conference on Types for Proofs and Programs, TYPES 2016, Novi Sad, Serbia, May 23-26, 2016, Book of Abstracts. EasyChair.
  • Devriese, D., Piessens, F., & Birkedal, L. (2016). Reasoning about Object Capabilities with Logical Relations and Effect Parametricity. In Proceedings of EuroS&P 2016.
  • Dezani-Ciancaglini, M., Ghilezan, S., Jaksic, S., Pantovic, J., & Yoshida, N. (2016). Denotational and Operational Preciseness of Subtyping: A Roadmap - Dedicated to Frank de Boer on the Occasion of His 60th Birthday. In Theory and Practice of Formal Methods - Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday (pp. 155--172).
  • Dodds, M., Jagannathan, S., Parkinson, M. J., Svendsen, K., & Birkedal, L. (2016). Verifying Custom Synchronisation Constructs Using Higher-Order Separation Logic. ACM Transactions on Programming Languages and Systems (TOPLAS), 38(2:4).
  • Cvetan Dunchev, Claudio Sacerdoti Coen, and Enrico Tassi. Implementing HOL in an Higher Order Logic Programming Language. In Logical Frameworks and Meta Languages: Theory and Practice, LFMTP ’16, page 10, Porto, Portugal, June 2016. ACM.
  • Dyckhoff, R. & Negri, S. (2016). A Cut-Free Sequent System for Grzegorczyk Logic, with an Application to the Gödel-McKinsey-Tarski Embedding. Journal of Logic and Computation,, 26(1), 169--187.
  • Espírito Santo, J. (2016). A Note on Strong Normalization in Classical Natural Deduction. In Proceedings Sixth International Workshop on Classical Logic and Computation, CL&C 2016, Porto, Portugal , 23th June 2016. (pp. 41--51).
  • Alexander Faithfull, Jesper Bengtson, Enrico Tassi, and Carst Tankink. Coqoon An IDE for interactive proof development in Coq. In TACAS, Eindhoven, Netherlands, April 2016.
  • D. Firsov, W. Jeltsch. Purely functional incremental computing. In F. Castor, Y. D. Liu, eds., Proc. of 20th Brazilian Symp. on Programming Languages, SBLP 2016 (Maringá, PR, Sept. 2016), v. 9889 of Lect. Notes in Comput. Sci., pp. 62-77. Springer, 2016.
  • D. Firsov, T. Uustalu, N. Veltri. Variations on Noetherianness. In R. Atkey, N. Krishnaswami, eds., Proc. of 6th Wksh. on Mathematically Structured Functional Programming, MSFP 2016 (Eindhoven, April 2016), v. 207 of Electron. Proc. in Theor. Comput. Sci., pp. 76-88. Open Publishing Assoc., 2016.
  • M. Gaboardi, S.-y. Katsumata, D. Orchard, F. Breuvart, T. Uustalu. Combining effects and coeffects via grading. In Proc. of 21st ACM SIGPLAN Int. Conf. on Functional Programming, ICFP '16 (Nara, Sept. 2016), pp. 476-489. ACM Press, 2016.
  • Ghani, N., Nordvall Forsberg, F., & Simpson, A. (2016). Comprehensive Parametric Polymorphism: Categorical Models and Type Theory. In FoSSaCS 2016 (pp. 3--19). Springer, Heidelberg.
  • Ghani, N., Nordvall Forsberg, F., & Orsanigo, F. (2016). Proof-relevant Parametricity. In A List of Successes That Can Change the World (pp. 109--131). Springer, Heidelberg.
  • Ghilezan, S., Jaksic, S., Pantovic, J., Perez, J. A., & Vieira, H. T. (2016). Dynamic Role Authorization in Multiparty Conversations. Formal Asp. Comput., 28(4), 643--667.
  • Girlando, M., Negri, S., Olivetti, N., & Risch, V. (2016). The Logic of Conditional Beliefs: Neighbourhood Semantics and Sequent Calculus. In Advances in Modal Logic 11, proceedings of the 11th conference on Advances in Modal Logic, held in Budapest, Hungary, August 30 - September 2, 2016 (pp. 322--341).
  • José Grimm. Implementation of Bourbaki’s Elements of Mathematics inCoq: Part Two, From Natural Numbers to Real Numbers. Journal of Formalized Reasoning, 9(2):52, 2016
  • Halmagrand, P. (2016). Soundly Proving B Method Formulae Using Typed Sequent Calculus. In 13th International Colloquium on Theoretical Aspects of Computing (ICTAC), Taipei, Taiwan, 2016 (pp. pp 196-213). Springer International Publishing.
  • Honsell, F., Lenisa, M., & Liquori, L. (2016). Implementing Cantor's Paradise. In 14th Asian Symposium on Programming Languages and Systems, Hanoi, Vietnam, November 21-23, 2016 (pp. 229--250). Springer LNCS.
  • Honsell, F., Lenisa, M., Liquori, L., & Scagnetto, I. (2016). An Open Logical Framework. Journal Logic Computation, 26(1), 293 - 335.
  • Honsell, F., Lenisa, M., Scagnetto, I., Liquori, L., & Maksimovic, P. (2016). An Open Logical Framework. J. Log. Comput., 26(1), 293--335. https://doi.org/10.1093/logcom/ext028
  • Honsell, F., Lenisa, M., Liquori, L., & Scagnetto, I. (2016). Implementing Cantor's Paradise. In Programming Languages and Systems, Cham, 2016 (pp. 229--250). Springer International Publishing.
  • Igried, B. & Setzer, A. (2016). Programming with Monadic CSP-style Processes in Dependent Type Theory. In Proceedings of the 1st International Workshop on Type-Driven Development, New York, NY, USA, 2016 (pp. 28--38). ACM.
  • W. Jeltsch. Abstract categorical semantics for resourceful functional reactive programming. J. of Log. and Algebraic Methods in Program., v. 85, n. 6, pp. 1177-1200, 2016.
  • Ji, K. (2016). Resolution in Solving Graph Problems. In 8th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2016), Toronto, Canada, 2016.
  • Jung, R., Krebbers, R., Birkedal, L., & Dreyer, D. (2016). Higher-Order Ghost State. In Proceedings of ICFP 2016.
  • Kraus, N. (2016). Constructions with Non-Recursive Higher Inductive Types. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS ’16). Association for Computing Machinery, New York, NY, USA, 595–604. DOI:https://doi.org/10.1145/2933575.2933586
  • Lapenta, S. & stean, I. L. (2016). Stochastic independence for probability MV-algebras. Fuzzy Sets and Systems, 298, 194-206.
  • Lapenta, S. & stean, I. L. (2016). Scalar extensions for algebraic structures of Łukasiewicz logics. Journal of Pure and Applied Algebra, 220, 1538-1553.
  • Liu, J., Dowek, G., Ji, K., & Jiang, Y. (2016). SCTL: Towards Combining Model Checking and Proof Checking. CoRR, abs/1606.08668.
  • Lourenco, C. B., Frade, M. J., & Pinto, J. S. (2016). Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach. In Programming Languages and Systems - 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings (pp. 41--67).
  • Lucanu, D., Serbanuta, T.-F., & Rosu, G. (2016). Towards a Kool Future. In Theory and Practice of Formal Methods - Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday (pp. 325--343). Springer.
  • Martin-Dorel, E. & Soloviev, S. (2016). A Formal Study of Boolean Games with Random Formulas as Payoff Functions. In 22nd International Conference on Types for Proofs and Programs, TYPES 2016, May 23-26, 2016, Novi Sad, Serbia (pp. 14:1--14:22).
  • Møgelberg, R. E. & Paviotti, M. (2016). Denotational Semantics of Recursive Types in Synthetic Guarded Domain Theory. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, New York, NY, USA, 2016 (pp. 317--326). ACM.
  • Miculan, M. & Peressotti, M. (2016). A Specification of Open Transactional Memory for Haskell. CoRR, abs/1602.05365. http://arxiv.org/abs/1602.05365
  • Negri, S. & Sbardolini, G. (2016). A System of Proof for Lewis Counterfactual. L. Felline et al. (eds) New Directions in Logic and the Philosophy of Science, 133-147.
  • Negri, S. (2016). Glivenko Sequent Classes in the Light of Structural Proof Theory. Archive for Mathematical Logic, 55(3-4), 461--473.
  • Negri, S. (2016). Proof Analysis Beyond Geometric Theories: from Rule Systems to Systems of Rules. The Review of Symbolic Logic, 9, 44-75.
  • Negri, S. & Sbardolini, G. (2016). Proof analysis for Lewis counterfactuals. The Review of Symbolic Logic, 9(1), 44--75.
  • Negri, S. (2016). Glivenko sequent classes in the light of structural proof theory. Archive for Mathematical Logic, 55(3-4), 461--473.
  • Negri, S. & von Plato, J. (2016). Cut elimination in sequent calculi with implicit contraction, with a conjecture on the origin of Gentzen’s altitude line construction. Concepts of Proof in Mathematics, Philosophy, and Computer Science. Ontos Mathematical Logic, Walter de Gruyter, Berlin, 269--290.
  • Negri, S. (2016). Non-normal modal logics: a challenge to proof theory. The Logica Yearbook, 125--140.
  • von Plato, J. (2016). Aristotle’s deductive logic: a proof-theoretical study. Concepts of Proof in Mathematics, Philosophy, and Computer Science, 6, 323.
  • Probst, D. & Schuster, P. (2016). Concepts of Proof in Mathematics, Philosophy, and Computer Science. Berlin: Walter de Gruyter.
  • Rijke, E. & Spitters, B. (2016). Homotopy type theory and the formalization of mathematics. Nieuw Archief voor Wiskunde, 5/17(3), 159 -- 164.
  • Rinaldi, D. & Schuster, P. (2016). A universal Krull--Lindenbaum theorem. J. Pure Appl. Algebra, 220, 3207--3232.
  • Rusu, V., Lucanu, D., Serbanuta, T.-F., Arusoaie, A., Stefanescu, A., & Rosu, G. (2016). Language definitions as rewrite theories. J. Log. Algebr. Meth. Program., 85(1), 98--120. https://doi.org/10.1016/j.jlamp.2015.09.001
  • Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee and German Andres Delbianco. Hoare-style Specifications as Correctness Conditions for Non-linearizable Concurrent Object. International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 92-110, 2016.
  • Setzer, A. (2015). The use of trustworthy principles in a revised Hilbert’s program. In Gentzen's Centenary (pp. 45-60). Springer, Cham.
  • Setzer A. (2016) How to Reason Coinductively Informally. In: Kahle R., Strahm T., Studer T. (eds) Advances in Proof Theory. Progress in Computer Science and Applied Logic, vol 28. Birkhäuser, Cham
  • Svendsen, K., Sieczkowski, F., & Birkedal, L. (2016). Transfinite Step-indexing: Decoupling Concrete and Logical Steps. In Proceedings of ESOP 2016.
  • Swan, A. W. (2016). An Algebraic Weak Factorisation System on 01-Substitution Sets: A Constructive Proof. Journal of Logic and Analysis, 8.
  • T. Uustalu. A divertimento on MonadPlus and nondeterminism. J. of Log. and Algebraic Methods in Program., v. 85, n. 5, part 2, pp. 1086-1094, 2016.
  • Wang, S., Dupin, L., Noel, M., Carroux, C., Renaud, L., Gehin, T., Meyer, A., Souteyrand, E., Vasseur, J.-J., Vergoten, G., Chevolot, Y., Morvan, F., & Vidal, S. (2016). Toward the Rational Design of Galactosylated Glycoclusters That Target Pseudomonas aeruginosa Lectin A (LecA): Influence of Linker Arms That Lead to Low-Nanomolar Multivalent Ligands. Chemistry - A European Journal, 22(33), 11785-11794. https://hal-udl.archives-ouvertes.fr/hal-02116180
  • Wang, S. (2016). Higher Order Proof Engineering: Proof Collaboration, Transformation, Checking and Retrieval. In AITP 2016 - Conference on Artificial Intelligence and Theorem Proving, Obergurgl, Austria, 2016.

2017

  • Abel, A., Vezzosi, A., & Winterhalter, T. (2017). Normalization by evaluation for sized dependent types. Proceedings of the ACM on Programming Languages, 1, 33. https://hal.archives-ouvertes.fr/hal-01596179
  • Abel, A., Adelsberger, S., & Setzer, A. (2017). Interactive programming in Agda -- Objects and graphical user interfaces. Journal of Functional Programming, 27.
  • Abel, A., Vezzosi, A., & Winterhalter, T. (2017). Normalization by Evaluation for Sized Dependent Types. In 23rd International Conference on Types for Proofs and Programs, TYPES 2017, Budapest, Hungary, May 29 -- June 1, 2017, Book of Abstracts. EasyChair.
  • Abiteboul, S. & Dowek, G. (2017). Le temps des algorithmes. Editions Le Pommier.
  • D. Ahman, C. Hritcu, K. Maillard, G. Martínez, G. Plotkin, J. Protzenko, A. Rastogi, N. Swamy. Dijkstra monads for free. In Proc. of 44th ACM SIGPLAN Symp. on Principles of Programming Languages, POPL '17 (Paris, Jan. 2017), pp. 515-529. ACM Press, 2017.
  • D. Ahman, T. Uustalu. Taking updates seriously. In R. Eramo, M. Johnson, eds., Proc. of 6th Int. Wksh. on Bidirectional Transformations, BX 2017 (Uppsala, Apr. 2017), v. 1827 of CEUR Wksh. Proc., pp. 59-73. RWTH Aachen, 2017.
  • German Andres Delbianco, Ilya Sergey, Aleksandar Nanevski and Anindya Banerjee. Concurrent Data Structures Linked in Time. European Conference on Object-Oriented Programming (ECOOP), pages 8:1-8:30, 2017
  • Allais, G., Chapman, J., McBride, C., & McKinna, J. (2017). Type-and-scope safe programs and their proofs. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017 (pp. 195--207).
  • Allais, G. (2017). Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic. In 23rd International Conference on Types for Proofs and Programs, TYPES 2017, May 29-June 1, 2017, Budapest, Hungary (pp. 1:1--1:22).
  • José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Gréegoire, Vincent Laporte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, and Pierre-Yves Strub. Jasmin: High-Assurance and High-Speed Cryptography. In CCS 2017 - Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, pages 1–17, Dallas, United States, October 2017.
  • José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Francois Dupressoir, Benjamin Gréegoire, Vincent Laporte, and Vitor Pereira. A Fast and Verified Software Stack for Secure Function Evaluation. In CCS 2017 - ACM SIGSAC Conference on Computer and Communications Security, Dallas, United States, October 2017. ACM.
  • Altenkirch T., Danielsson N.A., Kraus N. (2017) Partiality, Revisited. In: Esparza J., Murawski A. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2017. Lecture Notes in Computer Science, vol 10203. Springer, Berlin, Heidelberg
  • Altenkirch, T., Kaposi, A., & Kovács, A. (2017). Normalisation by Evaluation for a Type Theory with Large Elimination. In 23rd International Conference on Types for Proofs and Programs, TYPES 2017. Eötvös Loránd University.
  • Altenkirch, T. & Kaposi, A. (2017). Normalisation by Evaluation for Type Theory, in Type Theory. Logical Methods in Computer Science, Volume 13, Issue 4. https://lmcs.episciences.org/4005
  • Aman, B. & Ciobanu, G. (2017). A Probabilistic Approach of Behavioural Types. In 23rd International Conference on Types for Proofs and Programs (TYPES 2017).
  • Angeli, A., Dupin, L., Madaoui, M., Li, M., Vergoten, G., Wang, S., Meyer, A., Gehin, T., Vidal, S., Vasseur, J.-J., Chevolot, Y., & Morvan, F. (2017). Glycoclusters with Additional Functionalities for Binding to the LecA Lectin from Pseudomonas aeruginosa. ChemistrySelect, 2(32), 10420-10427. https://hal-udl.archives-ouvertes.fr/hal-02122269
  • Aristizábal, A., Biernacki, D., Lenglet, S., & Polesiuk, P. (2017). Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation. Logical Methods in Computer Science, 13(3). https://hal.inria.fr/hal-01590620
  • Arrighi, P. & Martiel, S. (2017). Quantum causal graph dynamics. Physical Review D, 96(2), 024026. https://hal.archives-ouvertes.fr/hal-01785461
  • Bahr, P., Grathwohl, H. B., & Møgelberg, R. E. (2017). The Clocks are Ticking: No More Delays!. In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (pp. 1--12).
  • Gilles Barthe, François Dupressoir, Sebastian Faust, Benjamin Grégoire, François-Xavier Standaert, and Pierre-Yves Strub. Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model. In Advances in Cryptology - EUROCRYPT 2017 - 36th Annual International Conference on the Theory and Applications of Cryptographic Techniques, pages 535–566, Paris, France, April 2017.
  • Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. Proving uniformity and independence by self-composition andcoupling. In LPAR 2017 - International Conferences on Logic for Programming, Artificial Intelligence and Reasoning, page 19, Maun, Botswana, May 2017
  • Gilles Barthe, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. Coupling proofs are probabilistic product programs. InPOPL 2017 - Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, volume 52, pages 161–174, Paris, France, January 2017. ACM
  • Bauer, A., Gross, J., Lumsdaine, P. L., Shulman, M., Sozeau, M., & Spitters, B. (2017). The HoTT Library: A Formalization of Homotopy Type Theory in Coq. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (pp. 164--172). Association for Computing Machinery.
  • van den Berg, B. (2017). A note on equality in finite-type arithmetic. MLQ Math. Log. Q., 63(3-4), 282--288. https://doi.org/10.1002/malq.201600080
  • van den Berg, B., Briseid, E., & Safarik, P. (2017). The strength of countable saturation. Arch. Math. Logic, 56(5-6), 699--711. https://doi.org/10.1007/s00153-017-0567-2
  • Sophie Bernard. Formalization of the Lindemann-Weierstrass Theorem. In Interactive Theorem Proving, Brasilia, Brazil, 2017
  • Yves Bertot, Laurence Rideau, and Laurent Théry. Distant decimals of π. Journal of Automated Reasoning, pages 1–45, 2017
  • Biendarra, J., Blanchette, J. C., Bouzy, A., Desharnais, M., Fleury, M., Holzl, J., Kuncar, O., Lochbihler, A., Meier, F., Panny, L., Popescu, A., Sternagel, C., Thiemann, R., & Traytel, D. (2017). Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic. In Frontiers of Combining Systems - 11th International Symposium, FroCoS 2017, Brasília, Brazil, September 27-29, 2017, Proceedings (pp. 3--21).
  • Biernacka, M., Biernacki, D., Lenglet, S., Polesiuk, P., Pous, D., & Schmitt, A. (2017). Fully Abstract Encodings of λ-Calculus in HOcore through Abstract Machines. In LICS 2017, Reykjavik, Iceland, 2017.
  • Biernacki, D., Lenglet, S., & Polesiuk, P. (2017). Proving Soundness of Extensional Normal-Form Bisimilarities. In Mathematical Foundations of Programming Semantics XXXIII, Ljubljana, Slovenia, 2017.
  • Bizjak, A. & Birkedal, L. (2017). On Models of Higher-Order Separation Logic. In Proceedings of MFPS2017.
  • Blanchette, J. C., Bouzy, A., Lochbihler, A., Popescu, A., & Traytel, D. (2017). Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants. In Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings (pp. 111--140).
  • Blanchette, J. C., Meier, F., Popescu, A., & Traytel, D. (2017). Foundational Nonuniform (Co)datatypes for Higher-Order Logic. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017 (pp. 1--12).
  • Blanchette, J. C., Fleury, M., & Traytel, D. (2017). Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL. In 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017, September 3-9, 2017, Oxford, UK (pp. 11:1--11:18).
  • Arthur Blot, Jean-Michel Muller, and Laurent Théry. Formal correctness of comparison algorithms between binary64 and decimal64 floating-point numbers. In Numerical Software Verification, number 10381 in Lecture Notes in Computer Science (LNCS), Heidelberg, Germany, July 2017. Springer
  • Blot, V. (2017). An interpretation of system F through bar recursion. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017 (pp. 1--12).
  • Blot, V. (2017). Realizability for Peano arithmetic with winning conditions in HON games. Ann. Pure Appl. Logic, 168(2), 254--277.
  • Branislava Živković, Milena Vujošević Janičić. Parallelization of Software Verification Tool LAV. In 23rd International Conference on Types for Proofs and Programs, TYPES 2017, Budapest, Hungary, May 29 -- June 1, 2017, Book of Abstracts. EasyChair.
  • Capriotti, P. and Kraus, N. (2017). Univalent higher categories via complete Semi-Segal types. Proc. ACM Program. Lang. 2, POPL, Article 44 (December 2017), 29 pages. DOI:https://doi.org/10.1145/3158132
  • J. Chapman, T. Uustalu, N. Veltri. Formalizing restriction categories. J. of Formaliz. Reason., v. 10, n. 1, pp. 1-36, 2017.
  • Chatzikyriakidis, S. & Luo, Z. (2017). Adjectival and Adverbial Modification: The View from Modern Type Theories. J. of Logic, Language and Information, 26(1).
  • Chatzikyriakidis, S. & Luo, Z. (2017). Identity Criteria of CNs: Quantification and Copredication. Workshop on Approaches to Coercion and Polysemy. Oslo.
  • Chatzikyriakidis, S. and Luo, Z. (eds., 2017). Modern Perspectives in Type Theoretical Semantics. Studies in Linguistics and Philosophy, Springer.
  • Chatzikyriakidis, S. & Luo, Z. (2017). On the Interpretation of Common Nouns: Types v.s. Predicates. In Modern Perspectives in Type-Theoretical Semantics, Springer..
  • Ciobaca, S. & Tudose, V. A. (2017). Automatically Constructing a Type System from the Small-Steps Semantics. In 23rd International Conference on Types for Proofs and Programs (TYPES 2017).
  • Cyril Cohen and Damien Rouhling. A Formal Proof in Coq of La Salle’s Invariance Principle. In Interactive Theorem Proving, Brasilia, Brazil, September 2017.
  • Diaconescu, D. & stean, I. L. (2017). Towards game semantics for nuanced logics. In 2017 IEEE International Conference on Fuzzy Systems (FUZZ-IEEE) (pp. 1-6).
  • Díaz-Caro, A. & Dowek, G. (2017). Typing Quantum Superpositions and Measurement. In TPNC 2017 - 6th International Conference on the Theory and Practice of Natural Computing, Prague, Czech Republic, 2017 (pp. 13). Springer.
  • Dinsdale-Young, T., Pinto, P., Andersen, K. J., & Birkedal, L. (2017). Caper: Automatic Verification for Fine-Grained Concurrency. In Proceedings of ESOP 2017.
  • Dowek, G. (2017). Rules and derivations in an elementary logic course. IfColog Journal of Logics and their Applications (FLAP), 4(1). https://hal.inria.fr/hal-01252124
  • Dowek, G. (2017). Analyzing individual proofs as the basis of interoperability between proof systems. In PxTP 2017 - Fifth Workshop on Proof eXchange for Theorem Proving, Brasilia, Brazil, 2017.
  • Dyckhoff, R. & Negri, S. (2017). Commentary on Grigori Mints' "Classical and Intuitionistic Geometric Logic". IfCoLog Journal of Logics and their Applications, 4, 1235--1239.
  • Espírito Santo, J. & Ghilezan, S. (2017). Characterization of Strong Normalizability for a Sequent Lambda Calculus with Co-control. In Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming, Namur, Belgium, October 09 - 11, 2017 (pp. 163--174).
  • Espírito Santo, J. (2017). The Polarized λ-calculus. Electr. Notes Theor. Comput. Sci., 332, 149--168.
  • Alexander Faithfull, Jesper Bengtson, Enrico Tassi, and Carst Tankink. Coqoon. International Journal on Software Tools for Technology Transfer, May 2017.
  • Gabrielli A., Maggesi M. (2017). Formalizing Basic Quaternionic Analysis. In: Ayala-Rincón M., Muñoz C. (eds) Interactive Theorem Proving. ITP 2017. Lecture Notes in Computer Science, vol 10499. Springer, Cham.
  • van Geest, M. & Swierstra, W. (2017). Generic packet descriptions: verified parsing and pretty printing of low-level data. In Proceedings of the 2nd ACM SIGPLAN International Workshop on Type-Driven Development (pp. 30--40).
  • Ghani, N., McBride, C., Nordvall Forsberg, F., & Spahn, S. (2017). Variations on Inductive-Recursive Definitions. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017) (pp. 63:1--63:13). Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik.
  • Gilbert, F. (2017). Proof certificates in PVS. In ITP 2017 - 8th International Conference on Interactive Theorem Proving, Brasilia, Brazil, 2017 (pp. 262-268). Springer.
  • Gilbert, F. (2017). Automated Constructivization of Proofs. In FoSSaCS 2017, Uppsala, Sweden, 2017.
  • Guerrieri, G., Paolini, L., & Rocca, S. R. D. (2017). Standardization and Conservativity of a Refined Call-by-Value lambda-Calculus. Logical Methods in Computer Science, 13(4).
  • Hadzihasanovic, A. & van den Berg, B. (2017). Nonstandard functional interpretations and categorical models. Notre Dame J. Form. Log., 58(3), 343--380. https://doi.org/10.1215/00294527-3870348
  • Honsell, F., Liquori, L., Maksimovic, P., & Scagnetto, I. (2017). LLFp: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads. Logical Methods in Computer Science, 13(3).
  • Honsell, F., Liquori, L., Maksimovic, P., & Scagnetto, I. (2017). LLFp: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads. Logical Methods in Computer Science.
  • Igried, B. & Setzer, A. (2017). Trace and Stable Failures Semantics for CSP-Agda. In Proceedings of the First Workshop on Coalgebra, Horn Clause Logic Programming and Types, Edinburgh, UK, 28-29 November 2016 (pp. 36-51). Open Publishing Association.
  • Jaksic, S., Pantovic, J., & Ghilezan, S. (2017). Linked Data Privacy. Mathematical Structures in Computer Science, 27(1), 33--53.
  • Jost, S., Vasconcelos, P. B., Florido, M., & Hammond, K. (2017). Type-Based Cost Analysis for Lazy Functional Languages. J. Autom. Reasoning, 59(1), 87--120.
  • Jouannaud, J.-P. & Strub, P.-Y. (2017). Coq without Type Casts: A Complete Proof of Coq Modulo Theory. In LPAR-21: 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, 2017.
  • Kammar, O. & Pretnar, M. (2017). No value restriction is needed for algebraic effects and handlers. J. Funct. Program., 27, e7. https://doi.org/10.1017/S0956796816000320
  • Kaposi, A., Kovács, A., Diviánszky, P., & Kőműves, B. (2017). Derivation of eEimination Principles From a Context. In 23rd International Conference on Types for Proofs and Programs, TYPES 2017. Eötvös Loránd University.
  • Kavvos, G. A. (2017). Dual-context calculi for modal logic. In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). IEEE.
  • Kavvos, G. A. (2017). On the Semantics of Intensionality. In Proceedings of the 20th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS) (pp. 550--566). Springer-Verlag Berlin Heidelberg.
  • Kraus, N., Escardó, M., Coquand, T., & Altenkirch, T. (2016). Notions of anonymous existence in Martin-Löf type theory. Logical Methods in Computer Science.
  • Kordic, B., Popovic, M., Ghilezan, S., & Basicevic, I. (2017). An Approach to Formal Verification of Python Software Transactional Memory. In Proceedings of the Fifth European Conference on the Engineering of Computer-Based Systems, ECBS 2017, Larnaca, Cyprus, August 31 - September 01, 2017 (pp. 13:1--13:10).
  • Krebbers, R., Jung, R., Bizjak, A., Jourdan, J.-H., Dreyer, D., & Birkedal, L. (2017). The Essence of Higher-Order Concurrent Separation Logic. In Proceedings of ESOP 2017.
  • Krebbers, R., Timany, A., & Birkedal, L. (2017). Interactive Proofs in Higher-Order Concurrent Separation Logic. In Proceedings of POPL 2017.
  • Krogh-Jespersen, M., Svendsen, K., & Birkedal, L. (2017). A Relational Model of Types-and-Effects in Higher-Order Concurrent Separation Logic. In Proceedings of POPL 2017.
  • Lapenta, S. & stean, I. L. (2017). Notes on divisible MV-algebras. Soft Computing, 21, 6213--6223.
  • Lepigre, R. (2017). PML 2 : Integrated Program Verification in ML. In 23rd International Conference on Types for Proofs and Programs (TYPES 2017), Budapest, Hungary, 2017 (pp. 27).
  • Lucanu, D., Rusu, V., & Arusoaie, A. (2017). A generic framework for symbolic execution: A coinductive approach. J. Symb. Comput., 80, 125--163. https://doi.org/10.1016/j.jsc.2016.07.012
  • Lungu, G. & Luo, Z. (2017). Definitional Extensions in Type Theorey Revisited. TYPES 2017, Budapest.
  • Luo, Z. & Soloviev, S. (2017). Dependent Event Types. In Logic, Language, Information, and Computation. WoLLIC 2017, LNCS. Springer, Berlin, Heidelberg.
  • Luo, Z. (2017). Modern Type Theories for Natural Language Semantics. Introductory course at ESSLLI 2017, Toulouse, France.
  • Luo, Z. & Soloviev, S. (2017). Dependent Event Types. In Logic, Language, Information, and Computation - 24th International Workshop, WoLLIC 2017, London, UK, July 18-21, 2017, Proceedings (pp. 216--228).
  • H. Maarand, T. Uustalu. Generating representative executions. In V. T. Vasconcelos, P. Haller, eds., Proc. of 10th Wksh. on Programming Language Approaches to Concurrency and Communication-Centric Software, PLACES 2017 (Uppsala, Apr. 2017), v. 246 of Electron. Proc. in Theor. Comput. Sci., pp. 39-48. Open Publishing Assoc., 2017.
  • Marco Maggesi (2017). A Formalization of Metric Spaces in HOL Light. Journal of Automated Reasoning, pp. 1-18, ISSN:0168-7433
  • Mansutti, A., Miculan, M., & Peressotti, M. (2017). Loose Graph Simulations. In Software Technologies: Applications and Foundations - STAF 2017 Collocated Workshops, Marburg, Germany, July 17-21, 2017, Revised Selected Papers (pp. 109--126). Springer.
  • Miraldo, V. C., Dagand, P.-É., & Swierstra, W. (2017). Type-directed diffing of structured data. In Proceedings of the 2nd ACM SIGPLAN International Workshop on Type-Driven Development (pp. 2--15).
  • Negri, S. (2017). The Intensional Side of Algebraic-Topological Representation Theorems. Synthese, 1--23.
  • Negri, S. (2017). Proof Theory for Non-normal Modal Logics: The Neighbourhood Formalism and Basic Results. IfCoLog Journal of Logics and their Applications, Mints' memorial issue, 4, 1241--1286.
  • Nuyts, A., Vezzosi, A., & Devriese, D. (2017). Parametric quantifiers for dependent type theory. PACMPL, 1(ICFP), 32:1--32:29.
  • Paolini, L., Piccolo, M., & Rocca, S. R. D. (2017). Essential and relational models. Mathematical Structures in Computer Science, 27(5), 626--650.
  • von Plato, J. (2017). From Gentzen to Jaskowski and back: algorithmic translation of derivations between the two main systems of natural deduction. Bulletin of the Section of Logic, 46(1/2), 65--74.
  • von Plato, J. (2017). In Husserl and Grassmann (pp. 93--109). Dordrecht: Springer Netherlands.
  • Qin, S., He, G., Chin, W.-N., Craciun, F., He, M., & Ming, Z. (2017). Automated specification inference in a combined domain via user-defined predicates. Science of Computer Programming, 148, 189--212.
  • Ren, I. Y., Koops, H. V., Volk, A., & Swierstra, W. (2017). In search of the consensus among musical pattern discovery algorithms. In Proceedings of the 18th International Society for Music Information Retrieval Conference (pp. 671--678).
  • Ricciotti, W. & Cheney, J. (2017). Strongly Normalizing Audited Computation. In CSL 2017 (pp. 36:1--36:21). Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik.
  • Rinaldi, D., Schuster, P., & Wessel, D. (2017). Eliminating disjunctions by disjunction elimination. Bull. Symb. Logic, 23(2), 181--200.
  • Rinaldi, D., Schuster, P., & Wessel, D. (2017). Eliminating disjunctions by disjunction elimination.
  • Soloviev, S. (2017). Grigori Mints, a Proof Theorist in the USSR: Some Personal Recollections in a Scientific Context. FLAP, 4(4).
  • Soloviev, S. (2017). Studies of Hilbert's epsilon-operator in the USSR. FLAP, 4(2).
  • Stolze, C., Liquori, L., Honsell, F., & Scagnetto, I. (2017). Towards a Logical Framework with Intersection and Union Types. In Proceedings of the Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, New York, NY, USA, 2017 (pp. 1--9). ACM.
  • Swierstra, W. & Dybjer, P. (2017). Special issue on Programming with Dependent Types Editorial. Journal of Functional Programming, 27, e15.
  • Traytel, D. (2017). Formal Languages, Formally and Coinductively. Logical Methods in Computer Science, 13(3).
  • T. Uustalu. Container combinatorics: monads and lax monoidal functors. In M. R. Mousavi, J. Sgall, eds., Proc. of 2nd IFIP WG 1.8 Int. Conf. on Topics in Theoretical Computer Science, TTCS 2017 (Tehran, Sept. 2017), v. 10608 of Lect. Notes in Comput. Sci., pp. 91-105. Springer, 2017.
  • T. Uustalu, N. Veltri. Finiteness and rational sequences, constructively. J. of Funct. Program., v. 27, article e13, 2017.
  • T. Uustalu, N. Veltri. Partiality and container monads. In B.-Y. E. Chang, ed., Proc. of 15th Asian Symp. on Programming Languages and Systems, APLAS 2017 (Suzhou, Nov. 2017), v. 10695 of Lect. Notes in Comput. Sci., pp. 406-425. Springer, 2017.
  • T. Uustalu, N. Veltri. The delay monad and restriction categories. In D. V. Hung, D. Kapur, eds., Proc. of 14th Int. Coll. on Theoretical Aspects of Computing, ICTAC 2017 (Hanoi, Oct. 2017), v. 10580 of Lect. Notes in Comput. Sci., pp. 32-50. Springer, 2017.
  • Von Plato, J. (2017). Saved from the cellar: Gerhard Gentzen’s shorthand notes on logic and foundations of mathematics. Springer.
  • Von Plato, J. (2017). The Great Formal Machinery Works: Theories of Deduction and Computation at the Origins of the Digital Age. Princeton University Press.
  • Swan, A. W. (2017). Some Brouwerian Counterexamples Regarding Nominal Sets in Constructive Set Theory. arXiv:1702.01556.

2018

  • Abel, A., Ohman, J., & Vezzosi, A. (2018). Decidability of conversion for type theory in type theory. Proceedings of the ACM on Programming Languages, 2(POPL), 23:1--23:29.
  • Abel, A. (2018). Resourceful Dependent Types. In 24th International Conference on Types for Proofs and Programs, TYPES 2018, Braga, Portugal, June 18-21, 2018, Book of Abstracts. EasyChair.
  • Adams, R. & Schupp, S. (2018). Constructing Independently Verifiable Privacy-Compliant Type Systems for Message Passing Between Black-Box Components. In Verified Software. Theories, Tools, and Experiments, Cham, 2018 (pp. 196--214). Springer International Publishing.
  • Adelsberger, S., Setzer, A., & Walkingshaw, E. (2018). Declarative GUIs: Simple, Consistent, and Verified. In Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, New York, NY, USA, 2018 (pp. 4:1--4:15). ACM.
  • Adelsberger, S., Setzer, A., & Walkingshaw, E. (2018). Developing GUI Applications in a Verified Setting. In Dependable Software Engineering. Theories, Tools, and Applications, Cham, 2018 (pp. 89--107). Springer International Publishing.
  • Adelsberger, S., Igried, B., Moser, M., Savenkov, V., & Setzer, A. (2018). Formal Verification for Feature-Based Composition of Workflows. In 2018 14th European Dependable Computing Conference (EDCC) (pp. 173-181).
  • Reynald Affeldt, Cyril Cohen, and Damien Rouhling. Formalization Techniques for Asymptotic Reasoning in Classical Analysis. Journal of Formalized Reasoning, October 2018.
  • Aguirre, A., Barthe, G., Birkedal, L., Bizjak, A., Gaboardi, M., & Garg, D. (2018). Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus. In Proceedings of ESOP 2018.
  • D. Ahman. Handling fibred algebraic effects. Proc. of ACM on Program. Lang., v. 2, n. POPL, article 7, 2018.
  • D. Ahman, C. Fournet, C. Hriţcu, K. Maillard, A. Rastogi, N. Swamy. Recalling a witness: foundations and applications of monotonic state. Proc. ACM Program. Lang., v. 2, n. POPL, article 65, 2018.
  • Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, Marco Maggesi. High-Level Signatures and Initial Semantics. CSL 2018, September 4-7, 2018 - Birmingham, GB
  • Ahrens, B., Matthes, R., & Mörtberg, A. (2018). From Signatures to Monads in UniMath. Journal of Automated Reasoning.
  • Allais, G., Atkey, R., Chapman, J., McBride, C., & McKinna, J. (2018). A type and scope safe universe of syntaxes with binding: their semantics and proofs. PACMPL, 2(ICFP), 90:1--90:30.
  • Allais, G. (2018). agdarsec -- Total Parser Combinators. In Journées Francophones des Langages Applicatifs 2018 (pp. 45--59).
  • Alpuim, J. & Swierstra, W. (2018). Embedding the refinement calculus in Coq. Science of Computer Programming, 164, 37 - 48. http://www.sciencedirect.com/science/article/pii/S0167642317300710
  • Altenkirch, T., Kaposi, A., Kovács, A., & von Raumer, J. (2018). Reducing Inductive-Inductive Types to Indexed Inductive Types. In 24th International Conference on Types for Proofs and Programs, TYPES 2018. University of Minho.
  • Altenkirch, T., Diviánszky, P., Kaposi, A., & Kovács, A. (2018). Constructing Inductive-Inductive Types using a Domain-Specific Type Theory. In 24th International Conference on Types for Proofs and Programs, TYPES 2018. University of Minho.
  • Altenkirch, T. & Kaposi, A. (2018). Towards a Cubical Type Theory without an Interval. In 21st International Conference on Types for Proofs and Programs (TYPES 2015) (pp. 3:1--3:27). Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik.
  • Altenkirch T., Capriotti P., Dijkstra G., Kraus N., Nordvall Forsberg F. (2018) Quotient Inductive-Inductive Types. In: Baier C., Dal Lago U. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2018. Lecture Notes in Computer Science, vol 10803. Springer, Cham. https://doi.org/10.1007/978-3-319-89366-2_16.
  • Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, and Nicolas Tabareau. Towards Certified Meta-Programming with Typed Template-Coq. In ITP 2018 - 9th Conference on Interactive Theorem Proving, volume 10895 of LNCS, pages 20–39, Oxford, United Kingdom, July 2018. Springer.
  • Antonio Di Nola, S. L. & stean, I. L. (2018). An analysis of the logic of Riesz spaces with strong unit. Journal of Pure and Applied Logic, 169, 216-234.
  • Antonio Di Nola, S. L. & stean, I. L. (2018). Infinitary logic and basically disconnected compact Hausdorff spaces. Journal of Logic and Computation, 28, 1275--1292.
  • Baillot, P., Benedetti, E. D., & Rocca, S. R. D. (2018). Characterizing polynomial and exponential complexity classes in elementary lambda-calculus. Inf. Comput., 261(Part), 55--77.
  • Bancerek, G., Naumowicz, A., & Urban, J. (2018). System Description: XSL-Based Translator of Mizar to LaTeX. In Intelligent Computer Mathematics - 11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings (pp. 1--6).
  • Cécile Baritel-Ruet, François Dupressoir, Pierre-Alain Fouque, and Benjamin Grégoire. Formal Security Proof of CMAC and Its Variants. In CSF 2018 - 31st EEE Computer Security Foundations Symposium, Oxford, United Kingdom, July 2018
  • Gilles Barthe, Sonia Belaïd, Thomas Espitau, Pierre-Alain Fouque, Benjamin Grégoire, Méelissa Rossi, and Mehdi Tibouchi. Masking the GLPLattice-Based Signature Scheme at Any Order. In Jesper Buus Nielsen and Vincent Rijmen, editors, Eurocrypt 2018 - 37th Annual International Conference on the Theory and Applications of Cryptographic Techniques, volume 10821 of Lecture Notes in Computer Science, pages 354–384, Tel Aviv, Israel, April 2018. Springer.
  • Gilles Barthe, Thomas Espitau, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. An Assertion-Based Program Logic for Probabilistic Programs. In Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018 Thessaloniki, Greece, April 14-20, 2018.
  • Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. Proving expected sensitivity of probabilistic programs. Proceedings of the ACM on Programming Languages, 2(POPL):1–29, January 2018.
  • Gilles Barthe, Xiong Fan, Joshua Gancher, Benjamin Grégoire, Charlie Jacomme, and Elaine Shi. Symbolic Proofs for Lattice-Based Cryptography. In CCS 2018 - Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security Canada, October 15-19, 2018,volume 17, pages 538–555, Toronto, Canada, October 2018. ACM Press 
 * Gilles Barthe, Benjamin Grégoire, and Vincent Laporte. Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic “Constant-Time”. In CSF 2018 - 31st IEEE Computer Security Foundations Symposium, Oxford, United Kingdom, July 2018
  • Bavendiek, K., Adams, R., & Schupp, S. (2018). Privacy-Preserving Architectures with Probabilistic Guaranties. In 2018 16th Annual Conference on Privacy, Security and Trust (PST) (pp. 1--10).
  • van den Berg, B. & Moerdijk, I. (2018). Univalent completion. Math. Ann., 371(3-4), 1337--1350. https://doi.org/10.1007/s00208-017-1614-3
  • van den Berg, B. (2018). Path categories and propositional identity types. ACM Trans. Comput. Log., 19(2), Art. 15, 32. https://doi.org/10.1145/3204492
  • van den Berg, B. & Moerdijk, I. (2018). Exact completion of path categories and algebraic set theory. Part I: Exact completion of path categories. J. Pure Appl. Algebra, 222(10), 3137--3181. https://doi.org/10.1016/j.jpaa.2017.11.017
  • van den Berg, B. & van Slooten, L. (2018). Arithmetical conservation results. Indag. Math. (N.S.), 29(1), 260--275. https://doi.org/10.1016/j.indag.2017.07.009
  • Berg, B. v. d. (2018). Univalent polymorphism.
  • Berger, U. & Setzer, A. (2018). Undecidability of Equality for Codata Types. In Coalgebraic Methods in Computer Science, Cham, 2018 (pp. 34--55). Springer International Publishing.
  • Yves Bertot. Formal Verification of a Geometry Algorithm: A Quest for Abstract Views and Symmetry in Coq Proofs. In ICTAC 2018 - International Colloquium on Theoretical of Computing, Stellenbosch, South Africa, October 2018.
  • Besten, M. d. (2018). A Quillen model structure for bigroupoids and pseudofunctors.
  • Bezem, M., Buchholtz, U., & Coquand, T. (2018). Syntactic Forcing Models for Coherent Logic. Indagationes Mathematicae, 29(6), 1441--1464.
  • Bezem, M., Coquand, T., & Huber, S. (2018). The Univalence Axiom in Cubical Sets. Journal of Automated Reasoning, 1--13.
  • M. Bezem, T. Coquand, K. Nakata, E. Parmann. Realizability at work:separating two constructive notions of finiteness. In S. Ghilezan, H. Geuvers, J. Ivetic, eds., Proc. of 22nd Int. Conf. on Types for Proofs and Programs, TYPES '16 (Novi Sad, May 2016), v. 97 of Leibniz Int. Proc. in Inf., article 6. Dagstuhl Publishing, 2018.
  • Birkedal, L., Bizjak, A., Clouston, R., Grathwohl, H. B., Spitters, B., & Vezzosi, A. (2018). Guarded Cubical Type Theory. Journal of Automated Reasoning, special issue of HoTT/UF.
  • Bizjak, A. & Birkedal, L. (2018). A Model of Guarded Recursion via Generalised Equilogical Spaces. Theoretical Computer Science, 772, 1--18.
  • Blanqui, F. (2018). Size-based termination of higher-order rewriting. Journal of Functional Programming. https://hal.inria.fr/hal-01424921
  • Blanqui, F. & Genestier, G. (2018). Termination of λΠ modulo rewriting using the size-change principle (work in progress). In 16th International Workshop on Termination, Oxford, United Kingdom, 2018 (pp. pp. 10-14).
  • Blot, V. & Laird, J. (2018). Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018 (pp. 95--104).
  • Bucciarelli, A., Kesner, D., & Rocca, S. R. D. (2018). Inhabitation for Non-idempotent Intersection Types. Logical Methods in Computer Science, 14(3).
  • Burel, G. (2018). Linking Focusing and Resolution with Selection. In 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018), Liverpool, United Kingdom, 2018 (pp. 9:1-9:14). Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik.
  • Chatzikyriakidis, S. & Luo, Z. (2018). Identity Criteria of Common Nouns and Dot-types for Copredication. Oslo Studies in Language, 10(2).
  • Ran Chen, Cyril Cohen, Jean-Jacques Levy, Stephan Merz, and Laurent Théry. Formal Proofs of Tarjan’s Strongly Connected Components Algorithm in Why3, Coq and Isabelle. In John Harrison, John O’Leary, and Andrew Tolmach, editors, ITP 2019 - 10th International Conference on Interactive Theorem Proving, volume 141, pages 13:1–13:19, Portland, United States, September 2019. Schloss Dagstuhl–Leibniz-Zentrum für Informatik
  • Ciaffaglione, A., Di Gianantonio, P., Honsell, F., Lenisa, M., & Scagnetto, I. (2018). Reversible Computation and Principal Types in λ!-calculus.. The Bulletin of Symbolic Logic.
  • Ciaffaglione, A., Honsell, F., Lenisa, M., & Scagnetto, I. (2018). The involutions-as-principal types/application-as-unification Analogy. In LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (pp. 254--270).
  • Ciobâca, S., Arusoaie, A., & Lucanu, D. (2018). Unification Modulo Builtins. In Logic, Language, Information, and Computation - 25th International Workshop, WoLLIC 2018, Bogota, Colombia, July 24-27, 2018, Proceedings (pp. 179--195). Springer.
  • Ciobâca, S. & Lucanu, D. (2018). A Coinductive Approach to Proving Reachability Properties in Logically Constrained Term Rewriting Systems. In Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings (pp. 295--311). Springer.
  • Cockx, J. & Abel, A. (2018). Eliminating dependent (co)pattern matching. Proceedings of the ACM on Programming Languages, 2(ICFP), 75:1--75:30.
  • Cockx, J. & Abel, A. (2018). Elaborating dependent (co)pattern matching. PACMPL, 2(ICFP), 75:1--75:30.
  • Costea, A., Chin, W.-N., Qin, S., & Craciun, F. (2018). Automated Modular Verification for Relaxed Communication Protocols. In Asian Symposium of Programming Languages and Systems, APLAS.
  • Craciun, F., Chin, W.-N., & Qin, S. (2018). Variant Region Types. In 23rd International Conference on Engineering of Complex Computer Systems, ICECCS.
  • Dalmonte, T., Olivetti, N., & Negri, S. (2018). Non-Normal Modal Logics: Bi-Neighbourhood Semantics and Its Labelled Calculi. In Advances in Modal Logic 12 (pp. 159--178). College Publications.
  • Dershowitz, N. & Jouannaud, J.-P. (2018). Graph Path Orderings. In 2nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Awassa, Ethiopia, 2018 (pp. 1-18).
  • Dershowitz, N. & Jouannaud, J.-P. (2018). Drags: A Simple Algebraic Framework For Graph Rewriting. In TERMGRAPH 2018 - 10th International Workshop on Computing with Terms and Graphs, Oxford, United Kingdom, 2018.
  • Boris Djalal. A Constructive Formalisation of Semi-algebraic Sets and Functions. In June Andronick and Amy Felty, editors, CPP 2018 - Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 240–251, Los Angeles, California, United States,January 2018. ACM.
  • Espírito Santo, J., Frade, M. J., & Pinto, L. (2018). Permutability in Proof Terms for Intuitionistic Sequent Calculus with Cuts. In 22nd International Conference on Types for Proofs and Programs, TYPES 2016, May 23-26, 2016, Novi Sad, Serbia (pp. 10:1--10:27). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik.
  • Espírito Santo, J., Matthes, R., & Pinto, L. (2018). Inhabitation in Simply-Typed Lambda-Calculus through a Lambda-Calculus for Proof Search. Mathematical Structures in Computer Science, 1--33.
  • Faissole, F. & Spitters, B. (2018). Preuves constructives de programmes probabilistes. In Journées Francophones des Langages Applicatifs.
  • Flor, J. P. P. & Swierstra, W. (2018). Verified Timing Transformations in Synchronous Circuits with λπ-Ware. In Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings (pp. 504--522).
  • Flor, J. P. P. & Swierstra, W. (2018). Verified Timing Transformations in Synchronous Circuits with λπ-Ware. In International Conference on Interactive Theorem Proving (pp. 504--522).
  • Frumin, D., Krebbers, R., & Birkedal, L. (2018). ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency. In Proceedings of LICS 2018.
  • Frumin, D., Geuvers, H., Gondelman, L., & van der Weide, N. (2018). Finite sets in homotopy type theory. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, Los Angeles, CA, USA, January 8-9, 2018 (pp. 201--214).
  • Ghilezan, S., Ivetic, J., Kasterovic, S., Ognjanovic, Z., & Savic, N. (2018). Probabilistic Reasoning About Simply Typed Lambda Terms. In Logical Foundations of Computer Science - International Symposium, LFCS 2018, Deerfield Beach, FL, USA, January 8-11, 2018, Proceedings (pp. 170--189).
  • Girlando, M., Negri, S., Olivetti, N., & Risch, V. (2018). Conditional Beliefs: from Neighbourhood Semantics to Sequent Calculus. The Review of Symbolic Logic, 11(4), 736--779.
  • Girlando, M., Olivetti, N., & Negri, S. (2018). Counterfactual Logic: Labelled and Internal Calculi, Two Sides of the Same Coin?. In Advances in Modal Logic 12 (pp. 291--310). College Publications.
  • Benjamin Grégoire, Kostas Papagiannopoulos, Peter Schwabe, and Ko Stoffelen. Vectorizing Higher-Order Masking. In COSADE 2018 - Constructive Side-Channel Analysis and Secure Design - 9th International Workshop, pages 23–43, Singapore, Singapore, April 2018.
  • Josée Grimm. Implementation of Bourbaki’s elements of mathematics in Coq:Part two, from natural numbers to real numbers. Journal of Formalized Reasoning, 9(2):1–52, 2016
  • Haagh, H., Karbyshev, A., Oechsner, S., Spitters, B., & Strub, P.-Y. (2018). Computer-Aided Proofs for Multiparty Computation with Active Security. In 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, United Kingdom, July 9-12, 2018 (pp. 119--131).
  • Honsell, F., Liquori, L., Maksimovic, P., & Scagnetto, I. (2018). Plugging-in proof development environments using Locks in LF. Mathematical Structures in Computer Science, 28(9), 1578--1605.
  • Honsell, F., Liquori, L., Stolze, C., & Scagnetto, I. (2018). The Delta-Framework. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018) (pp. 37:1--37:21).
  • Huang, D., Morrisett, G., & Spitters, B. (2018). An Application of Computable Distributions to the Semantics of Probabilistic Programs. arXiv.
  • Igried, B. & Setzer, A. (2018). Defining trace semantics for CSP-Agda. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016), Dagstuhl, Germany, 2018 (pp. 12:1--12:23). Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik.
  • Jakubuv, J. & Kaliszyk, C. (2018). Towards a Unified Ordering for Superposition-Based Automated Reasoning. In Mathematical Software - ICMS 2018 - 6th International Conference, South Bend, IN, USA, July 24-27, 2018, Proceedings (pp. 245--254).
  • Jonathan Sterling, B. S. (2018). Normalization by gluing for free λ-theories.
  • Jung, R., Krebbers, R., Jourdan, J.-H., Bizjak, A., Birkedal, L., & Dreyer, D. (2018). Iris from the Ground Up: A Modular Foundation for Higher-Order Concurrent Separation Logic. Journal of Functional Programming.
  • Kaposi, A. & Kovács, A. (2018). A Syntax for Higher Inductive-Inductive Types. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), Dagstuhl, Germany, 2018 (pp. 20:1--20:18). Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik.
  • Karbyshev, A., Svendsen, K., Askarov, A., & Birkedal, L. (2018). Compositional Non-Interference for Concurrent Programs via Separation and Framing. In Proceedings of POST 2018.
  • S. Katsumata, T. Sato, T. Uustalu. Codensity lifting of monads and its dual. Log. Methods in Comput. Sci., v. 14, n. 4, article 6, 2018.
  • Kovács, A. (2018). Closure Conversion for Dependent Type Theory, With Type-Passing Polymorphism. In 24th International Conference on Types for Proofs and Programs, TYPES 2018. University of Minho.
  • Kraus, N. and Altenkirch, T. (2018). Free Higher Groups in Homotopy Type Theory. LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 599--608. https://doi.org/10.1145/3209108.3209183
  • Lepigre, R. & Raffalli, C. (2018). Abstract Representation of Binders in OCaml using the Bindlib Library. Electronic Proceedings in Theoretical Computer Science, 274, 42-56. https://hal.inria.fr/hal-01972050
  • Daniel R. Licata, Ian Orton, Andrew M. Pitts, and Bas Spitters. Internal Universes in Models of Homotopy Type Theory. In Hélène Kirchner, editor, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), volume 108 of Leibniz International Proceedings in Informatics (LIPIcs), pages 22:1–22:17, Dagstuhl, Germany, 2018.
  • Lourenco, C. B., Frade, M. J., Nakajima, S., & Pinto, J. S. (2018). A Generalized Approach to Verification Condition Generation. In 2018 IEEE 42nd Annual Computer Software and Applications Conference, COMPSAC 2018, Tokyo, Japan, 23-27 July 2018, Volume 1 (pp. 194--203).
  • Lungu, G. (2018). Subtyping in Signatures. Ph.D. dissertation, Royal Holloway, Univ. of London.
  • Lungu, G. & Luo, Z. (2018). On Subtyping in Type Theories with Canonical Objects. Post-proceedings of the 22nd Int. Conf. on Types for Proofs and Programs, Leibniz International Proceedings in Informatics.
  • Luo, Z. (2018). Formal Semantics in Modern Type Theories (and Event Semantics in MTT-framework). Invited talk at LACompLing18, Stockholm.
  • Luo, Z. (2018). MTT-semantics in Martin-Lof's Type Theory with HoTT's Logic. Proc of LACompLing 2018, Stockholm.
  • Luo, Z. (2018). Substructural Calculi with Dependent Types. Linearity & TLLA (affiliaed with FLoC), Oxford.
  • H. Maarand, T. Uustalu. Certified Foata normalization for generalized traces. In A. Dutle, C. Muñoz, A. Narkawicz, eds., Proc. of 10th NASA Formal Methods Symp., NFM 2018 (Newport News, VA, Apr. 2018), v. 10811 of Lect. Notes in Comput. Sci., pp. 299-314. Springer, 2018.
  • Mannaa, B. & Møgelberg, R. E. (2018). The Clocks They Are Adjunctions Denotational Semantics for Clocked Type Theory. In 3rd International Conference on Formal Structures for Computation and Deduction, {FSCD} 2018, July 9-12, 2018, Oxford, {UK} (pp. 23:1--23:17).
  • Marinković, B., Ognjanović, Z., & Glavan, P. (2018). Correctness and Strong Completeness for Logic of Time and Knowledge. In Universal Logic, UNILOG 2018, Vichy, France, June 16-26, 2018, Proceedings.
  • Martin-Dorel, É. & Soloviev, S. (2018). A Formal Study of Boolean Games with Random Formulas as Payoff Functions. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016).
  • Negri, S. & Orlandelli, E. (2018). Proof theory for quantified monotone modal logics. Logic Journal of the IGPL.
  • Nuyts, A. & Devriese, D. (2018). Degrees of Relatedness: A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018 (pp. 779--788).
  • Ian Orton and Andrew M. Pitts. Axioms for Modelling Cubical Type Theory in a Topos. Logical Methods in Computer Science, Volume 14, Issue 4, December 2018.
  • Ian Orton and Andrew M. Pitts. Decomposing the Univalence Axiom. In Andreas Abel, Fredrik Nordvall Forsberg, and Ambrus Kaposi, editors, 23rd International Conference on Types for Proofs and Programs (TYPES2017), volume 104 of Leibniz International Proceedings in Informatics (LIPIcs), pages 6:1–6:19, Dagstuhl, Germany, 2018.
  • Pinto, L. & Uustalu, T. (2018). A Proof-Theoretic Study of Bi-Intuitionistic Propositional Sequent Calculus. J. Log. Comput., 28(1), 165--202.
  • von Plato, J. (2018). Real numbers and projective spaces: Intuitionistic reasoning with undecidable basic relations. Indagationes Mathematicae, 29(6), 1546--1554.
  • Ren, Y., Koops, H. V., Bountouridis, D., Volk, A., Swierstra, W., & Veltkamp, R. C. (2018). Feature analysis of repeated patterns in Dutch folk songs using Principal Component Analysis. In Proceedings of the 8th International Workshop on Folk Music Analysis (FMA2018) (pp. 86--88).
  • Ricciotti, W. & Cheney, J. (2018). Explicit Auditing. In Theoretical Aspects of Computing -- ICTAC 2018. Springer International Publishing.
  • Rinaldi, D., Schuster, P., & Wessel, D. (2018). Eliminating disjunctions by disjunction elimination. Indag. Math. (N.S.), 29(1), 226--259.
  • Andrei Rodin, On Constructive Axiomatic Method, Logique et Analyse vol 61, no 242 (2018), p. 201-231.
  • Andrei Rodin, Two “Styles” of axiomatization: Rules versus Axioms. A Modern Perspective. Bulletin of Symbolic Logic, vol. 24, n. 2 (2018), p. 263-264.
  • Damien Rouhling. A Formal Proof in Coq of a Control Function for the Inverted Pendulum. In CPP 2018 - 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 1–14, Los Angeles, United States, January 2018.
  • Schuster, P. & Wessel, D. (2018). Suzumura consistency, an alternative approach. J. Appl. Logics -- IfCoLog, 5(1), 263--286.
  • Schuster, P. & Wessel, D. (2018). A general extension theorem for directed-complete partial orders. Rep. Math. Logic, 53, 79--96.
  • Setzer, A. (2018). Modelling Bitcoin in Agda. arXiv, arXiv:1804.06398, 27. https://arxiv.org/abs/1804.06398
  • Skorstengaard, L., Devriese, D., & Birkedal, L. (2018). Reasoning about a Capability Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management (without OS Support). In Proceedings of ESOP 2018.
  • Skorstengaard, L., Devriese, D., & Birkedal, L. (2018). Reasoning About a Machine with Local Capabilities. In Programming Languages and Systems. Springer International Publishing.
  • Soloviev, S. V. & Malakhovski, J. (2018). Automorphisms of types and their applications. In Zapiski POMI (pp. 287--308).
  • Mirko Spasić and Milena Vujošević Janičić. First steps towards proving functional equivalence of embedded SQL. In 24th International Conference on Types for Proofs and Programs, TYPES 2018, Braga, Portugal, June 18-21, 2018, Book of Abstracts. EasyChair.
  • Swan, A. W. (2018). Lifting Problems in Grothendieck Fibrations. arXiv:1802.06718.
  • Swan, A. W. (2018). W-Types with Reductions and the Small Object Argument. arXiv:1802.07588.
  • Swan, A. W. (2018). On dividing by two in constructive mathematics. arXiv:1804.04490.
  • Rathjen, M. & Swan, A. W. (2018). Lifschitz Realizability as a Topological Construction. arXiv:1806.10047.
  • Swan, A. W. (2018). Separating Path and Identity Types in Presheaf Models of Univalent Type Theory. arXiv:1808.00920.
  • Swan, A. W. (2018). Identity Types in Algebraic Model Structures and Cubical Sets. arXiv:1808.00915.
  • Thiré, F. (2018). Sharing a Library between Proof Assistants: Reaching out to the HOL Family *. Electronic Proceedings in Theoretical Computer Science, 274, 57 - 71. https://hal.inria.fr/hal-01929714
  • Thomas Dinsdale-Young, Bas Spitters, D. T. & Thomsen, S. E. (2018). WIP: Formalizing the Concordium consensus protocol in Coq. CoqPL '19.
  • Timany, A., Stefanesco, L., Krogh-Jespersen, M., & Birkedal, L. (2018). A Logical Relation for Monadic Encapsulation of State: Proving contextual equivalences in the presence of runST. In Proceedings of POPL.
  • Timany, A., Stefanesco, L., Krogh-Jespersen, M., & Birkedal, L. (2018). A Logical Relation for Monadic Encapsulation of State: Proving Contextual Equivalences in the Presence of RunST. PACMPL, 2(POPL), 64:1--64:28.
  • Tomé Cortiñas, C. & Swierstra, W. (2018). From algebra to abstract machine: a verified generic construction. In Proceedings of the 3rd ACM SIGPLAN International Workshop on Type-Driven Development (pp. 78--90).
  • Taichi Uemura, Cubical Assemblies, a Univalent and Impredicative Universe and a Failure of Propositional Resizing, 24th International Conference on Types for Proofs and Programs (TYPES 2018), 7:1--7:20, 2019, volume 130.
  • T. Uustalu, N. Veltri, N. Zeilberger. The sequent calculus of skew-monoidal categories. Electron. Notes in Theor. Comput. Sci., v. 341 (S. Staton, ed., Proc. of 34th Conf. on Mathematical Foundations of Programming Semantics, MFPS XXXIV, Halifax, NS, June 2018), pp. 345-370, 2018.
  • Von Plato, J. (2018). Kurt Gödel’s First Steps in Logic: Formal Proofs in Arithmetic and Set Theory through a System of Natural Deduction. Bulletin of Symbolic Logic, 24(3), 319--335.
  • Von Plato, J. (2018). In search of the sources of incompleteness. In Proc. Int. Cong. of Math (pp. 21--30).
  • Xu, Z., Ren, K., Qin, S., & Craciun, F. (2018). CDGDroid: Android Malware Detection Based on Deep Learning using CFG and DFG. In International Conference on Formal Engineering Methods, ICFEM.
  • Xue, T., Luo, Z., & Chatzikyriakidis, S. (2018). Propositional Forms of Judgemental Interpretations. NLCS18 (affiliated with FLoC), Oxford.

2019

  • D. Ahman, T. Uustalu. Decomposing comonad morphisms. In M. Roggenbach, A. Sokolova, eds., Proc. of 8th Conf. on Algebra and Coalgebra in Computer Science, CALCO 2019 (London, June 2019), v. 139 of Leibniz Int. Proc. in Inf., article 14. Dagstuhl Publishing, 2019.
  • Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, Marco Maggesi. Modular specification of monads through higher-order presentations. FSCD 2019 - 4th International Conference on Formal Structures for Computation and Deduction, Jun 2019, Dortmund, Germany. pp.1-16.
  • Ahrens, B. & Lumsdaine, P. L. (2019). Displayed Categories. Logical Methods in Computer Science, Volume 15, Issue 1.
  • Ahrens, B., Frumin, D., Maggesi, M., & Van der Weide, N. (2019). Bicategories in Univalent Foundations. In 4th International Conference on Formal Structures for Computation and Deduction.
  • Alessi, Fabio et al. LF+ in Coq for "fast and loose" reasoning. Journal of Formalized Reasoning, [S.l.], v. 12, n. 1, p. 11 - 51, jan. 2020. ISSN 1972-5787.
  • José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Grégoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, and Serdar Tasiran. A Machine-Checked Proof of Security for AWS Key Management Service. In ACM CCS 2019 - 26th ACM Conference on Computer and Communications Security, volume 16, pages 63–78, London, United Kingdom, November 2019. ACM Press.
  • José Bacelar Almeida, Cécile Baritel-Ruet, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Alley Stoughton, and Pierre-Yves Strub. Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3. In CCS 2019 - 26th ACM Conference on Computer and Communications Security, pages 1607–1622, London, United Kingdom, November 2019. ACM Press.
  • Altenkirch T. (2019) Naïve Type Theory. In: Centrone S., Kant D., Sarikaya D. (eds) Reflections on the Foundations of Mathematics. Synthese Library (Studies in Epistemology, Logic, Methodology, and Philosophy of Science), vol 407. Springer, Cham
  • Altenkirch T., Boulier S., Kaposi A., Tabareau N. (2019) Setoid Type Theory—A Syntactic Translation. In: Hutton G. (eds) Mathematics of Program Construction. MPC 2019. Lecture Notes in Computer Science, vol 11825. Springer, Cham
  • Annenkov, D. & Spitters, B. (2019). Deep and Shallow Embeddings in Coq. TYPES2019.
  • Bahr, P., Graulund, C., & Møgelberg, R. (2019). Simply RaTT: A Fitch-style Modal Calculus for Reactive Programming. ICFP.
  • João Barbosa, Mário Florido, and Vítor Santos Costa. A three-valued semantics for typed logic programming. In Bart Bogaerts, Esra Erdem, Paul Fodor, Andrea Formisano, Giovambattista Ianni, Daniela Inclezan, GermánVidal, Alicia Villanueva, Marina de Vos, and Fangkai Yang, editors, Proceedings 35th International Conference on Logic Programming (Technical Communications), ICLP 2019 Technical Communications, Las Cruces, NM, USA, September 20-25, 2019, volume 306 of EPTCS, pages 36–51, 2019.
  • Gilles Barthe, Sonia Belaïd, Gaëtan Cassiers, Pierre-Alain Fouque, Benjamin Grégoire, and François-Xavier Standaert. Automated Verification of Higher-Order Masking in Presence of Physical Defaults. In ESORICS 2019 - 24th European Symposium on Research in Computer Security, pages 300–318, Luxembourg, Luxembourg, September 2019.
  • Gilles Barthe, Benjamin Grégoire, Charlie Jacomme, Steve Kremer, and Pierre-Yves Strub. Symbolic Methods in Computational Cryptography Proofs. In CSF 2019 - 32nd IEEE Computer Security Foundations Symposium, pages 136–13615, Hoboken, United States, June 2019. IEEE.
  • Basold, H. (2019). Coinduction in Flow: The Later Modality in Fibrations.
  • Bauer, A. & Swan, A. (2019). Every metric space is separable in function realizability. Logical Methods in Computer Science, Volume 15, Issue 2. https://lmcs.episciences.org/5501
  • Florent Bréhard, Assia Mahboubi, Damien Pous. A certificate-based approach to formally verified approximations. ITP 2019 - Tenth International Conference on Interactive Theorem Proving, Sep 2019, Portland, United States. pp.1-19.
  • Van den Berg, Benno . A Kuroda-style j-translation. Arch. Math. Logic 58 (2019), no. 5-6, 627--634.
  • Van den Berg, B. & Sanders, S. (2019). Reverse mathematics and parameter-free transfer. Ann. Pure Appl. Logic, 170(3), 273--296. https://doi.org/10.1016/j.apal.2018.10.003
  • Ulrich Berger, Ralph Matthes, and Anton Setzer. Martin Hofmann’s Case for Non-Strictly Positive Data Types. In Peter Dybjer, José Espírito Santo, and Luís Pinto, editors, 24th International Conference on Types for Proofs and Programs (TYPES 2018), volume 130 of Leibniz International Proceedings in Informatics (LIPIcs), pages 1:1–1:22, Dagstuhl, Germany, 2019.
  • Bezem, Marc; Coquand, Thierry. Skolem’s Theorem in Coherent Logic. Fundamenta Informaticae 2019 ;Volum 170.(1-3) s. 1-14.
  • Biernacki, D., Lenglet, S., & Polesiuk, P. (2019). Proving Soundness of Extensional Normal-Form Bisimilarities. Logical Methods in Computer Science.
  • Biernacki, D., Lenglet, S., & Polesiuk, P. (2019). Diacritical Companions. In Mathematical Foundations of Programming Semantics, London, United Kingdom, 2019.
  • Biernacki, D., Lenglet, S., & Polesiuk, P. (2019). A Complete Normal-Form Bisimilarity for State. In FoSSaCS, Prague, Czech Republic, 2019.
  • Bizjak, A., Gratzer, D., Krebbers, R., & Birkedal, L. (2019). Iron: managing obligations in higher-order concurrent separation logic. PACMPL, 3(POPL), 65:1--65:30.
  • Blanchette, J. C., Gheri, L., Popescu, A., & Traytel, D. (2019). Bindings as Bounded Natural Functors. PACMPL, 3(POPL), 22:1--22:34.
  • Blanqui, F., Genestier, G., & Hermant, O. (2019). Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting. In 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany. (pp. 9:1--9:21).
  • A. Buldas, D. Firsov, R. Laanoja, H. Lakk, A. Truu. A new approach to constructing digital signature schemes. In N. Attrapadung, T. Yagi, eds., Proc. of 14th Int. Wksh. on Security, IWSEC 2019 (Tokyo, Aug. 2019), v. 11689 of Lect. Notes in Comput. Sci., pp. 363-373. Springer, 2019.
  • Buruiana, A.-S. & Ciobâca, S. (2019). Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics. In Proceedings Fifth International Workshop on Rewriting Techniques for Program Transformations and Evaluation, Oxford, England, 8th July 2018 (pp. 1-16). Open Publishing Association.
  • Sunjay Cauligi, Gary Soeller, Brian Johannesmeyer, Fraser Brown, Riad S Wahby, John Renner, Benjamin Grégoire, Gilles Barthe, Ranjit Jhala, and Deian Stefan. FaCT: A DSL for Timing-Sensitive Computation. In PLDI 2019 - 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, Phoenix, United States, June 2019.
  • Mathesis Universalis, Computability and Proof: Gottfried Leibniz's philosophy of logic in the Digital Age. S. Centrone, S. Negri, D. Sarikaya, and P. Schuster (eds.), 2019, Springer. 374 p. (Synthese Library)
  • J. Chapman, T. Uustalu, N. Veltri. Quotienting the delay monad by weak bisimilarity. Math. Struct. in Comput. Sci., v. 29, n. 1, pp. 67-92, 2019.
  • Chatzikyriakidis, S. and Luo, Z. (2019). From Montague Semantics to Modern Type Theories: A Meaningful Comparison. Advanced Course in Language & Logic at ESSLLI 2019. Riga, Latvia.
  • Chatzikyriakidis, S. and Luo, Z. (2019). Gradability in MTT-Semantics. TbiLLC 2019: Thirteenth International Tbilisi Symposium on Language, Logic and Computation. Tbilisi.
  • Zheng Cheng, Massimo Tisi, Rémi Douence. CoqTL: A Coq DSL for Rule-Based Model Transformation. Software and Systems Modeling, Springer Verlag, In press, pp.1-15.
  • Cyrille Chenavier, Maxime Lucas. The Diamond Lemma for non-terminating rewriting systems using deterministic reduction strategies. IWC 2019 - 8th International Workshop on Confluence, Jun 2019, Dortmund, Germany. pp.1-5.
  • Alberto Ciaffaglione, Pietro Di Gianantonio, Furio Honsell, Marina Lenisa, and Ivan Scagnetto. lambda!-calculus, Intersection Types, and Involutions. In Herman Geuvers, editor, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), volume 131 of Leibniz International Proceedings in Informatics (LIPIcs), pages 15:1–15:16, Dagstuhl, Germany, 2019.
  • Colin, S., Lepigre, R., & Scherer, G. (2019). Unboxing Mutually Recursive Type Definitions in OCaml. In JFLA 2019 - 30 èmes journées francophones des langages applicatifs, Les Rousses, France, 2019.
  • T. Dalmonte, S. Negri, N. Olivetti and G.L. Pozzato. PRONOM: proof-search and countermodel generation for non-normal modal logics. AIIA 2019, 18th International Conference of the Italian Association for Artificial Intelligence.
  • T. Dalmonte, S. Negri, N. Olivetti and G.L. Pozzato. Proof-search and countermodel generation for non-normal modal logics: The theorem prover PRONOM. Intelligenza Artificiale, IOS Press, in press.
  • Dinsdale-Young, T., Spitters, B., Thompson, S. E., & Tschudi, D. (2019). WIP: Formalizing the Concordium consensus protocol in Coq.
  • Paul Downen, Zena M. Ariola, Silvia Ghilezan. The Duality of Classical Intersection and Union Types. Fundamenta Informaticae 170(1-3): 39-92 (2019)
  • Eremondi, J., Swierstra, W., & Hage, J. (2019). A framework for improving error messages in dependently-typed languages. Open Computer Science, 9, 1-32.
  • José Espírito Santo, Ralph Matthes, and Luís Pinto. "Decidability of several concepts of finiteness for simple types." Fundamenta Informaticae 170.1-3 (2019): 111-138.
  • José Espírito Santo, Luís Pinto, Tarmo Uustalu, Modal Embeddings and Calling Paradigms, in H. Geuvers (ed.), Proc. 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019 LIPIcs, vol. 131, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 18:1--18:20, 2019.
  • Faggian, C. & Rocca, S. R. D. (2019). Lambda Calculus and Probabilistic Computation. LICS 2019: 1-13.
  • Frumin, D. & van den Berg, B. (2019). A homotopy-theoretic model of function extensionality in the effective topos. Math. Structures Comput. Sci., 29(4), 588--614. https://doi.org/10.1017/S0960129518000142
  • Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, Nicolas Tabareau. Definitional Proof-Irrelevance without K. Proceedings of the ACM on Programming Languages, ACM, 2019, POPL'19, pp.1-28.
  • Ghani, N., Nordvall Forsberg, F., & Orsanigo, F. (2019). Universal properties for universal types in bifibrational parametricity. Mathematical Structures in Computer Science, 29(6), 810--827.
  • Silvia Ghilezan, Svetlana Jaksic, Jovanka Pantovic, Alceste Scalas, Nobuko Yoshida. Precise subtyping for synchronous multiparty sessions. Journal of Logical and Algebraic Methods in Programming 104: 127-173 (2019).
  • Gratzer, D., Sterling, J., & Birkedal, L. (2019). Implementing a Modal Dependent Type Theory.
  • Ferruccio Guidi, Claudio Sacerdoti Coen, and Enrico Tassi. Implementing Type Theory in Higher Order Constraint Logic Programming. Mathematical Structures in Computer Science, 29(8):1125–1150, March 2019.
  • Gylterud, Håkon Robbestad. Multisets in type theory. Mathematical proceedings of the Cambridge Philosophical Society (Print) 2019 s. 1-18
  • R. Kaarsgaard, N. Veltri. En garde! Unguarded iteration for reversible computation in the delay monad. In G. Hutton, ed., Proc. of 13th Int. Conf. on Mathematics of Program Construction, MPC 2019 (Porto, Oct. 2019), v. 11825 of Lect. Notes in Comput. Sci., pp. 366-384. Springer, 2019.
  • Koen Jacobs, Andreas Nuyts, and Dominique Devriese. How to do proofs: Practically proving properties about effectful programs’ results (functional pearl). In Proceedings of the 4th ACM SIGPLAN International Workshop on Type-Driven Development, TyDe 2019, page 1–13, New York, NY, USA, 2019. Association for Computing Machinery.
  • Kaposi, A., Huber, S., & Sattler, C. (2019). Gluing for Type Theory. In 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany. (pp. 25:1--25:19).
  • Kaposi, A., Kovacs, A., & Altenkirch, T. (2019). Constructing quotient inductive-inductive types. PACMPL, 3(POPL), 2:1--2:24.
  • Kaposi A., Kovács A., Kraus N. (2019) Shallow Embedding of Type Theory is Morally Correct. In: Hutton G. (eds) Mathematics of Program Construction. MPC 2019. Lecture Notes in Computer Science, vol 11825. Springer, Cham. https://doi.org/10.1007/978-3-030-33636-3_12
  • Bruce M. Kapron and Florian Steinberg. Type-two polynomial-time and restricted lookahead. Theoretical Computer Science, 813:1 – 19, 2020.
  • Simona Kašterović, Michele Pagani: The Discriminating Power of the Let-in Operator in the Lazy Call-by-Name Probabilistic λ-Calculus, FSCD 2019 - International Conference on Formal Structures for Computation and Deduction, Dortmund, Germany, June 24-30, 2019
  • Kavvos, G. A. (2019). Modalities, Cohesion, and Information Flow. Proceedings of the ACM on Programming Languages, 3(POPL).
  • Serge Kovalyov and Andrei Rodin, Truth and Justification in Knowledge Representation, S.O. Kuznetsov, A. Napoli and S. Rudolph (eds.) Proceedings of the 7th Workshop “What can Formal Concept Analysis do for Artificial Intelligence?” (August 10-17, 2019, Macao, China) , in CEUR Vol. 2529 pp.45-56.
  • Kraus, N. and von Raumer, J. "Path Spaces of Higher Inductive Types in Homotopy Type Theory," 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Vancouver, BC, Canada, 2019, pp. 1-13, doi: 10.1109/LICS.2019.8785661.
  • Branislav Kordic, Miroslav Popovic, Silvia Ghilezan. Formal Verification of Python Software Transactional Memory Based on Timed Automata. Acta Polytechnica Hungarica Vol. 16, No. 7: 197-216 (2019).
  • Larchey-Wendling D., Matthes R. (2019) Certification of Breadth-First Algorithms by Extraction. In: Hutton G. (eds) Mathematics of Program Construction. MPC 2019. Lecture Notes in Computer Science, vol 11825. Springer, Cham
  • Luo, Z. (2019). Proof Irrelevance in Type-Theoretical Semantics. Studies in Computational Intelligence (SCI). Springer.
  • Luo, Z. (2019). Formal Semantics in Modern Type Theories: An Overview. Third Conference on Proof-Theoretic Semantics (PTS19), Tubingen.
  • Luo, Z. and Soloviev, S. (2019). Dependent Event Types in Event Semantics. TYPES 2019. Oslo.
  • Lynge, A. & Spitters, B. (2019). Universal Algebra in HoTT. TYPES2019.
  • M. Girlando, S. N. & Sbardolini, G. (2019). Uniform labelled calculi for conditional and counterfactual logics. WoLLIC 2019, LNCS 11541.
  • H. Maarand, T. Uustalu. Certified normalization of generalized traces. Innov. in Syst. and Softw. Engin., v. 15, n. 3-4, pp. 253-265, 2019.
  • Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote. Formally Verified Approximations of Definite Integrals. Journal of Automated Reasoning, Springer Verlag, 2019, 62 (2), pp.281-300.
  • K. Maillard, D. Ahman, R. Atkey, G. Martínez, C. Hritcu, E. Rivas, É. Tanter. Dijkstra monads for all. Proc. of ACM on Program. Lang., v. 3, n. ICFP, article 104, 2019.
  • Ian Malakhovsky. On the Expressive Power of Indexed Applicative and Monadic Structures. (Supervisor S. Soloviev.) University of Toulouse 3 Paul Sabatier and IRIT, 2019.
  • Giulio Manzonetto, Michele Pagani, Simona Ronchi Della Rocca. New Semantical Insights Into Call-by-Value λ-Calculus.Fundam. Inform. 170(1-3): 241-265 (2019)
  • G. Martínez, D. Ahman, V. Dumitrescu, N. Giannarakis, C. Hawblitzel, C. Hritcu, M. Narasimhamurthy, Z. Paraskevopoulou, C. Pit-Claudel, J. Protzenko, T. Ramananandro, A. Rastogi, N. Swamy. Meta-F*: proof automation with SMT, tactics, and metaprograms. In L. Caires, ed., Proc. of 28th Europ. Symp. on Programming, ESOP 2019 (Prague, Apr. 2019), v. 11423 of Lect. Notes in Comput. Sci., pp. 30-59. Springer, 2019.
  • Miraldo, V. C. & Swierstra, W. (2019). An Efficient Algorithm for Type-Directed Structural Diffing. Proc. ACM Program. Lang., 6(ICFP).
  • Møgelberg, R. E. & Paviotti, M. (2019). Denotational Semantics of Recursive Types in Synthetic Guarded Domain Theory. Mathematical Structures in Computer Science, 29(3), 465--510.
  • Møgelberg, R. E. & Veltri, N. (2019). Bisimulation as Path Type for Guarded Recursive Types. Proceedings of the ACM on Programming Languages, 3(POPL), 4.
  • Aleksandar Nanevski, Anindya Banerjee, German Andres Delbianco and Ignacio Fabregas. Specifying Concurrent Programs in Separation Logic: Morphisms and Simulations. International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2019.
  • S. Negri. Geometric rules in infinitary logic. In Arnon Avron on Semantics and Proof Theory of Non-Classical Logics, Outstanding Contributions to Logic. Springer. In press.
  • S. Negri and E. Orlandelli. Proof theory for quantified monotone modal logics. Logic Journal of the IGPL, vol. 27, pp. 478--506, 2019.
  • S. Negri, M. Girlando and G. Sbardolini. Uniform labelled calculi for conditional and counterfactual logics. R. Iemhoff et al. (eds), WoLLIC 2019, LNCS 11541.
  • S. Negri, E. Pavloviç. Alternative axiomatizations for logics of agency, {\em Foundations of Science} Special Issue, R.Giuntini, P. Graziani, G. Sergioli, S. Sozzo (eds), submitted.
  • S. Negri, E. Pavloviç. Proof-theoretic analysis of the logics of agency: the deliberative STIT. Studia Logica, in press.
  • Negri, S. & von Plato, J. (2019). From mathematical axioms to mathematical rules of proof: recent developments in proof analysis. Philosophical Transactions of the Royal Society A, 377(2140), 20180037.
  • Ian Orton and Andrew M. Pitts. Models of Type Theory Based on Moore Paths. Logical Methods in Computer Science, Volume 15, Issue 1, January 2019.
  • Orlova, N. & Soloviev, S. (2019). Logic and logicians in Russia before 1917: Living in a wider world. Historia Mathematica, 46, 38-55.
  • Pierre-Marie Pédrot, Nicolas Tabareau. The Fire Triangle: How to Mix Substitution, Dependent Elimination, and Effects. Proceedings of the ACM on Programming Languages, ACM, 2020, pp.1-28.
  • Pierre-Marie Pédrot, Nicolas Tabareau, Hans Fehrmann, Éric Tanter. A Reasonably Exceptional Type Theory. Proceedings of the ACM on Programming Languages, ACM, 2019, Issue ICFP, 3, pp.1-29.
  • Pientka, B., Thibodeau, D., Abel, A., Ferreira, F., & Zucchini, R. (2019). A Type Theory for Defining Logics and Proofs. In Logic in Computer Science (LICS'19).
  • Piotrowski, B., Urban, J., Brown, C. E., & Kaliszyk, C. (2019). Can Neural Networks Learn Symbolic Rewriting?. In Proceedings of the ICML 2019 Workshop on Learning and Reasoning with Graph-Structured Representations.
  • Marko Popovic, Miroslav Popovic, Silvia Ghilezan, Branislav Kordic. Formal Verification of Local and Distributed Python Software Transactional Memories. Revue roumaine des sciences techniques Série Électrotechnique et Énergétique, issue 4, 2019: 423-428.
  • Miroslav Popovic, Marko Popovic, Silvia Ghilezan, Branislav Kordic. Formal Verification of Python Software Transactional Memory Serializability Based on the Push/Pull Semantic Model. European Conference on the Engineering of Computer Based Systems ECBS 2019: 6:1-6:8
  • Andrei Rodin, Extra-logical proof-theoretic semantics in HoTT , Piecha, Thomas; Schroeder-Heister, Peter (eds.) Proceedings of conference Proof Theoretic Semantics: Assessments and Future Perspectives : Tübingen, March 27-30, 2019, p. 45, 765-786.
  • Andrei Rodin, Models of HoTT and the Constructive View of Theories, in: Stefania Centrone, Deborah Kant and Deniz Sarikaya (eds.) Reflections on the Foundations of Mathematics: Univalent Foundations, Set Theory and General Thoughts, Springer, Synthese Library vol.407., pp. 191-219.
  • Andrei Rodin, Formal Proof-Verification and Mathematical Intuition: the Case of Univalent Foundations, in: 16th International Congress on Logic, Methodology and Philosophy of Science and Technology Bridging across Academic Cultures (Prague, August 5-10, 2019), Book of Abstracts, p. 418
  • Schrijvers, T., d. S. Oliveira, B. C., Wadler, P., & Marntirosian, K. (2019). COCHIS: Stable and coherent implicits. J. Funct. Program., 29, e3.
  • Schuster, P. & Wessel, D. (2019). Some forms of excluded middle for linear orders. Math. Log. Quart., 65(1), 105--107.
  • Schuster, P. & Wessel, D. (2019). Syntax for Semantics: Krull's Maximal Ideal Theorem.
  • Lau Skorstengaard, Dominique Devriese, and Lars Birkedal. Reasoning about a machine with local capabilities: Provably safe stack and return pointer management. ACM Trans. Program. Lang. Syst., 42(1), December 2019
  • Skorstengaard, L., Devriese, D., & Birkedal, L. (2019). StkTokens: Enforcing Well-bracketed Control Flow and Stack Encapsulation Using Linear Capabilities. Proc. ACM Program. Lang., 3(POPL), 19:1--19:28. http://doi.acm.org/10.1145/3290332
  • Soloviev, S. (2019). Automorphisms of Types in Certain Type Theories and Representation of Finite Groups. Mathematical Structures in Computer Science, 29(4), 511--551.
  • S. Soloviev, J. Malakhovski. Automorphisms of Types and Their Applications. J. of Math. Sciences (Springer), 240(5), 692-706 (2019).
  • Florian Steinberg, Holger Thies, and Laurent Théry. Quantitative continuity and Computable Analysis in Coq. In ITP 2019 - Tenth International Conference on Interactive Theorem Proving, Portland, United States, September 2019.
  • Swan, A. W. & Uemura, T. (2019). On Church's Thesis in Cubical Assemblies. arXiv:1905.03014.
  • Swierstra, W. & Baanen, T. (2019). A predicate transformer semantics for effects. Proc. ACM Program. Lang., 6(ICFP).
  • Nicolas Tabareau, Éric Tanter. Chemical foundations of distributed aspects. Distributed Computing, Springer Verlag, In press, 32 (Issue 3), pp.193-216.
  • Enrico Tassi. Deriving proved equality tests in Coq-elpi: Stronger induction principles for containers in Coq. In ITP 2019 - 10th International Conference on Interactive Theorem Proving, Portland, United States, September 2019.
  • Veltri, N. & Van der Weide, N. (2019). Guarded Recursion in Agda via Sized Types. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), Dagstuhl, Germany, 2019 (pp. 32:1--32:19). Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik.
  • Vezzosi, A., Mortberg, A., & Abel, A. (2019). Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types. In ICFP.
  • Van der Weide, N. & Geuvers, H. (2019). The Construction of Set-Truncated Higher Inductive Types.
  • Winterhalter, T., Sozeau, M., & Tabareau, N. (2019). Eliminating Reflection from Type Theory. In CPP 2019 - The 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Lisbonne, Portugal, 2019 (pp. 91-103). ACM.
  • Centrone, S., Negri, S., Sarikaya, D., & Schuster, P. (forthcoming). Mathesis Universalis, Computability and Proof. Springer.
  • Powell, T., Schuster, P., & Wiesnet, F. (forthcoming). An algorithmic approach to the existence of ideal objects in commutative algebra. In 26th Workshop on Logic, Language, Information and Computation (WoLLIC 2019), Utrecht, Netherlands, 2--5 July 2019, Proceedings. Springer.

2020

  • D. Ahman, A. Bauer. Runners in action. In P. Müller, ed., Proc. of 29th Europ. Symp. on Programming, ESOP 2020 (Dublin, Apr. 2020), v. 12075 of Lect. Notes in Comput. Sci., pp. 29-55. Springer, 2020.
  • Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, Marco Maggesi. Reduction Monads and Their Signatures. Proceedings of the ACM on Programming Languages, ACM, 2020, pp.1-29.
  • Benno van den Berg. Univalent polymorphism, Annals of Pure and Applied Logic171 (2020), no 6.
  • Birkedal, L., Clouston, R., Mannaa, B., Ejlers Møgelberg, R., Pitts, A., & Spitters, B. (2020). Modal dependent type theory and dependent right adjoints. Mathematical Structures in Computer Science, 30(2), 118-138. doi:10.1017/S0960129519000197
  • Christian Doczkal and Damien Pous. Completeness of an Axiomatization of Graph Isomorphism via Graph Rewriting in Coq. InCPP 2020 - 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’20), New Orleans, LA, United States, January 2020.
  • Fiore M.P., Pitts A.M., Steenkamp S.C. (2020) Constructing Infinitary Quotient-Inductive Types. In: Goubault-Larrecq J., König B. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2020. Lecture Notes in Computer Science, vol 12077. Springer, Cham
  • D. Firsov, A. Buldas, A. Truu, R. Laanoja. Verified security of BLTs signature scheme. In Proc. of 9th ACM SIGPLAN Int. Conf. on Certified Programs and Proofs, CPP 2020 (New Orleans, LA, Jan. 2020), pp. 244-257. ACM Press, 2020.
  • Forssell, Jon Henrik; Gylterud, Håkon Robbestad; Spivak, David I. Type theoretical databases. Journal of Logic and Computation 2020
  • Silvia Ghilezan, Jelena Ivetic, Simona Kasterovic, Zoran Ognjanovic, Nenad Savic. Towards Probabilistic Reasoning in Type Theory - The Intersection Type Case Foundations of Information and Knowledge Systems - 11th International Symposium, FoIKS 2020, Dortmund, Germany, February 2020, Lecture Notes in Computer Science 12012: 122--139 (2020)
  • Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, Lars Birkedal, Multimodal Dependent Type Theory, accepted at LICS 2020
  • Guilhem Jaber. SyTeCi: Automating Contextual Equivalence for Higher-Order Programs with References. Proceedings of the ACM on Programming Languages, ACM, In press, 28, pp.1-28.
  • Jonas Kastberg Hinrichsen, Jesper Bengtson and Robbert Krebbers. Actris: Session-Type Based Reasoning in Separation Logic. In POPL 2020.
  • Maclean, H. and Luo, Z. (2020). Subtype Universes. TYPES20. Turin.
  • Nordvall Forsberg, F., Xu, C & Ghani, N. (2020). Three equivalent ordinal notation systems in cubical Agda. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020). Association for Computing Machinery, New York, NY, USA, 172–185.
  • S. Katsumata, E. Rivas, T. Uustalu. Interaction laws of monads and comonads. In Proc. of 35th Ann. ACM/IEEE Symp. on Logic in Computer Science, LICS 2020 (Saarbrücken, July 2020), ACM Press, to appear.
  • Marco Maggesi, Enrico Tassi. Private types in Higher Order Logic Programming. TEASE-LP 2020
  • Andrew M. Pitts. Typal heterogeneous equality types. ACM Trans. Comput.Logic, 21(3), April 2020.
  • Mirko Spasić, Milena Vujošević Janičić. Verification Supported Refactoring of Embedded SQL. Software Quality Journal, Springer. (2020)
  • Milena Vujošević Janičić. Concurrent Bug Finding Based on Bounded Model Checking. Int’l Journal of Software Engineering and Knowledge Engineering. (2020)
  • Milena Vujosevic-Janicic, Filip Maric. Regression verification for automated evaluation of students programs. Comput. Sci. Inf. Syst. 17(1): 205-227 (2020)
  • Anders Mörtberg, Loïc Pujet. Cubical Synthetic Homotopy Theory. CPP 2020 - 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2020, New Orleans, United States. pp.1-14.
  • Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, et al.. The MetaCoq Project. Journal of Automated Reasoning, Springer Verlag, 2020.
  • Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, Théo Winterhalter. Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq. Proceedings of the ACM on Programming Languages, ACM, 2020, pp.1-28.
  • T. Uustalu, N. Veltri, N. Zeilberger. The sequent calculus of skew-monoidal categories. In C. Casadio, P. J. Scott, eds., [Joachim Lambek Memorial Volume], Outstanding Contributions to Logic, Springer, to appear.
  • T. Uustalu, N. Veltri, N. Zeilberger. Eilenberg-Kelly reloaded. In Electron. Notes in Theor. Comput. Sci. (P. Johann, ed., Proc. of 36th Conf. on Mathematical Foundations of Programming Semantics, MFPS XXXVI, Paris, June 2020), to appear.
  • N. Veltri, A. Vezzosi. Formalizing π-calculus in guarded cubical Agda. In Proc. of 9th ACM SIGPLAN Int. Conf. on Certified Programs and Proofs, CPP 2020 (New Orleans, LA, Jan. 2020), pp. 270-283. ACM Press, 2020. doi:10.1145/3372885.3373814
  • N. Voorneveld. From equations to distinctions: two interpretations of effectful computations. In M. S. New, S. Lindley, eds., Proc. of 8th Wksh. on Mathematically Structured Functional Programming, MSFP 2020 (Dublin, Apr. 2020), v. 317 of Electron. Proc. in Theor. Comput. Sci., pp. 1-17. Open Publ. Assoc., 2020.
  • Simona Kasterovic, Silvia Ghilezan, Kripke semantics and completeness for full simply typed lambda calculus, To appear in Journal of Logic and Computation, Volume 30, issue 8, 2020.
  • Niels van der Weide, Constructing Finitary 1-Truncated Higher Inductive Types as Groupoid Quotients, accepted at LICS 2020.

2021

  • Dan Frumin, Robbert Krebbers and Lars Birkedal. Compositional Non-Interference for Fine-Grained Concurrent Programs. To appear in Security & Privacy 2021.