print · source · 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

  • 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. (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., Adelsberger, S., & Setzer, A. (2017). Interactive programming in Agda -- Objects and graphical user interfaces. Journal of Functional Programming, 27, e8.
  • 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. & Winterhalter, T. (2016). An Extension of Martin-L\"of 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.
  • 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.
  • 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., 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).
  • 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).
  • 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.
  • Ahrens, B., Matthes, R., & Mörtberg, A. (2018). From Signatures to Monads in UniMath. Journal of Automated Reasoning.
  • Ahrens, B. & Lumsdaine, P. L. (2019). Displayed Categories. Logical Methods in Computer Science, Volume 15, Issue 1. https://lmcs.episciences.org/5252
  • Ahrens, B., Frumin, D., Maggesi, M., & van der Weide, N. (). Bicategories in Univalent Foundations.
  • 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).
  • 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., 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. (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).
  • 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., & 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. (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. (2017). Normalisation by Evaluation for Type Theory, in Type Theory. Logical Methods in Computer Science, Volume 13, Issue 4. https://lmcs.episciences.org/4005
  • 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.
  • 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 FoSSaCS 2018.
  • Aman, B. & Ciobanu, G. (2017). A Probabilistic Approach of Behavioural Types. In 23rd International Conference on Types for Proofs and Programs (TYPES 2017).
  • Annenkov, D. & Spitters, B. (). Deep and Shallow Embeddings in Coq. TYPES2019.
  • 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.
  • 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
  • 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).
  • 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.
  • 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
  • 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. & 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
  • 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
  • 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
  • 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.
  • 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.
  • 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).
  • 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).
  • 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. (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.
  • Biernacki, D., Lenglet, S., & Polesiuk, P. (2017). Proving Soundness of Extensional Normal-Form Bisimilarities. In Mathematical Foundations of Programming Semantics XXXIII, Ljubljana, Slovenia, 2017.
  • 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.
  • Birkedal, L., Jaber, G., Sieczkowski, F., & Thamsborg, J. (2016). A Kripke Logical Relation for Effect-Based Program Transformations. Information and Computation.
  • Birkedal, L., Bizjak, A., Clouston, R., Gratwohl, H. B., Spitters, B., & Vezzosi, A. (2016). Guarded Cubical Type Theory. In Proceedings of Types 2016.
  • Bizjak, A. & Birkedal, L. (2018). A Model of Guarded Recursion via Generalised Equilogical Spaces. Theoretical Computer Science, 772, 1--18.
  • Bizjak, A. & Birkedal, L. (2017). On Models of Higher-Order Separation Logic. In Proceedings of MFPS2017.
  • 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.
  • 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).
  • Blanchette, J. C., Gheri, L., Popescu, A., & Traytel, D. (2019). Bindings as Bounded Natural Functors. PACMPL, 3(POPL), 22:1--22:34.
  • 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).
  • 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.
  • 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).
  • 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).
  • Bucciarelli, A., Kesner, D., & Rocca, S. R. D. (2018). Inhabitation for Non-idempotent Intersection Types. Logical Methods in Computer Science, 14(3).
  • 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.
  • Centrone, S., Negri, S., Sarikaya, D., & Schuster, P. (forthcoming). Mathesis Universalis, Computability and Proof. Springer.
  • Chatzikyriakidis, S. & Luo, Z. (2018). Identity Criteria of Common Nouns and Dot-types for Copredication. Oslo Studies in Language, 10(2).
  • 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. & Luo, Z. (2017). On the Interpretation of Common Nouns: Types v.s. Predicates. In Modern Perspectives in Type-Theoretical Semantics, Springer.
  • Chatzikyriakidis, S. & Luo, Z. (2016). Proof Assistants for Natural Language Semantics. LACL 2016. Nancy.
  • 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).
  • 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).
  • 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.
  • 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
  • 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.
  • Clouston, R., Mannaa, B., Mögelberg, R. E., Pitts, A. M., & Spitters, B. (2018). Modal Dependent Type Theory and Dependent Right Adjoints. CoRR, abs/1804.05236.
  • 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. (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.
  • 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.
  • Craciun, F. & Glodean, G. (2010). Towards Compiling Region Types into RTSJ-compliant Java Code. In Symbolic and Numeric Algorithms for Scientific ComputingSYNASC.
  • 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.
  • Daniel Huang, Greg Morrisett, B. S. (). An Application of Computable Distributions to the Semantics of Probabilistic Programs.
  • 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).
  • 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).
  • Dinsdale-Young, T., Pinto, P., Andersen, K. J., & Birkedal, L. (2017). Caper: Automatic Verification for Fine-Grained Concurrency. In Proceedings of ESOP 2017.
  • 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).
  • 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.
  • Dyckhoff, R. & Negri, S. (2017). Commentary on Grigori Mints' "Classical and Intuitionistic Geometric Logic". IfCoLog Journal of Logics and their Applications, 4, 1235--1239.
  • Eremondi, J., Swierstra, W., & Hage, J. (2019). A framework for improving error messages in dependently-typed languages. Open Computer Science, 9, 1-32.
  • Esp\irito 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.
  • 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. (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).
  • Espírito Santo, J. (2017). The Polarized λ-calculus. Electr. Notes Theor. Comput. Sci., 332, 149--168.
  • Faggian, C. & Rocca, S. R. D. (2019). Lambda Calculus and Probabilistic Computation. CoRR, abs/1901.02853.
  • 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. & 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
  • 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., Nordvall Forsberg, F., & Orsanigo, F. (2019). Universal properties for universal types in bifibrational parametricity. Mathematical Structures in Computer Science, 29(6), 810--827.
  • 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.
  • 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., 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).
  • 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. (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.
  • 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).
  • 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).
  • Haagh, H., Karbyshev, A., Oechsner, S., Spitters, B., & Strub, P.-Y. (2018). Computer-aided proofs for multiparty computation with active security. In 2018 IEEE 31st Computer Security Foundations Symposium (CSF) (pp. 119--131).
  • 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., 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., 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., Lenisa, M., Liquori, L., & Scagnetto, I. (2016). Implementing Cantor's Paradise. In Programming Languages and Systems, Cham, 2016 (pp. 229--250). Springer International Publishing.
  • Honsell, F., Liquori, L., Maksimovic, P., & Scagnetto, I. (). LLFp: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads. Logical Methods in Computer Science.
  • 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. (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.
  • 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.
  • 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.
  • Jaksic, S., Pantovic, J., & Ghilezan, S. (2017). Linked Data Privacy. Mathematical Structures in Computer Science, 27(1), 33--53.
  • 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. (). Normalization by gluing for free λ-theories.
  • 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.
  • 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.
  • Jung, R., Krebbers, R., Birkedal, L., & Dreyer, D. (2016). Higher-Order Ghost State. In Proceedings of ICFP 2016.
  • 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.
  • 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.
  • 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.
  • Kavvos, G. A. (2019). Modalities, Cohesion, and Information Flow. Proceedings of the ACM on Programming Languages, 3(POPL).
  • 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).
  • 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.
  • 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. (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.
  • Lapenta, S. & stean, I. L. (2017). Notes on divisible MV-algebras. Soft Computing, 21, 6213--6223.
  • Licata, D. R., Orton, I., Pitts, A. M., & Spitters, B. (2018). Universes in Models of Homotopy Type Theory. FSCD.
  • 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).
  • 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).
  • 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
  • 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.
  • 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.
  • Lungu, G. & Luo, Z. (2017). Definitional Extensions in Type Theorey Revisited. TYPES 2017, Budapest.
  • 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. (2018). Formal Semantics in Modern Type Theories (and Event Semantics in MTT-framework). Invited talk at LACompLing18, Stockholm.
  • Luo, Z. & Soloviev, S. (2017). Dependent Event Types. In Logic, Language, Information, and Computation. WoLLIC 2017, LNCS. Springer, Berlin, Heidelberg.
  • 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.
  • 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).
  • Lynge, A. & Spitters, B. (). Universal Algebra in HoTT. TYPES2019.
  • M. Girlando, S. N. & Sbardolini, G. (). Uniform labelled calculi for conditional and counterfactual logics. WoLLIC 2019, LNCS 11541.
  • 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.
  • 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, 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).
  • 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).
  • Miculan, M. & Peressotti, M. (2016). A Specification of Open Transactional Memory for Haskell. CoRR, abs/1602.05365. http://arxiv.org/abs/1602.05365
  • 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).
  • Miraldo, V. C. & Swierstra, W. (2019). An Efficient Algorithm for Type-Directed Structural Diffing. Proc. ACM Program. Lang., 6(ICFP).
  • Negri, S. & von Plato, J. (). Hilbert's Last Problem. Philosophical Transactions of the Royal Society.
  • 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. (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.
  • Negri, S. & Orlandelli, E. (2018). Proof theory for quantified monotone modal logics. Logic Journal of the IGPL.
  • 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.
  • 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.
  • 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).
  • Nuyts, A., Vezzosi, A., & Devriese, D. (2017). Parametric quantifiers for dependent type theory. PACMPL, 1(ICFP), 32:1--32:29.
  • Orlova, N. & Soloviev, S. (2019). Logic and logicians in Russia before 1917: Living in a wider world. Historia Mathematica, 46, 38-55.
  • Paolini, L., Piccolo, M., & Rocca, S. R. D. (2017). Essential and relational models. Mathematical Structures in Computer Science, 27(5), 626--650.
  • 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).
  • Pinto, L. & Uustalu, T. (2018). A Proof-Theoretic Study of Bi-Intuitionistic Propositional Sequent Calculus. J. Log. Comput., 28(1), 165--202.
  • 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.
  • 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. (2018). Real numbers and projective spaces: Intuitionistic reasoning with undecidable basic relations. Indagationes Mathematicae, 29(6), 1546--1554.
  • 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).
  • von Plato, J. (2016). Aristotle’s deductive logic: a proof-theoretical study. Concepts of Proof in Mathematics, Philosophy, and Computer Science, 6, 323.
  • von Plato, J. (2017). In Husserl and Grassmann (pp. 93--109). Dordrecht: Springer Netherlands.
  • 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.
  • Probst, D. & Schuster, P. (2016). Concepts of Proof in Mathematics, Philosophy, and Computer Science. Berlin: Walter de Gruyter.
  • 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.
  • Rathjen, M. & Swan, A. W. (2018). Lifschitz Realizability as a Topological Construction. arXiv:1806.10047.
  • 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).
  • 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. (2017). Strongly Normalizing Audited Computation. In CSL 2017 (pp. 36:1--36:21). Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik.
  • Ricciotti, W. & Cheney, J. (2018). Explicit Auditing. In Theoretical Aspects of Computing -- ICTAC 2018. Springer International Publishing.
  • 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., & Wessel, D. (2017). Eliminating disjunctions by disjunction elimination. Bull. Symb. Logic, 23(2), 181--200.
  • Rinaldi, D., Schuster, P., & Wessel, D. (2018). Eliminating disjunctions by disjunction elimination. Indag. Math. (N.S.), 29(1), 226--259.
  • Rinaldi, D. & Schuster, P. (2016). A universal Krull--Lindenbaum theorem. J. Pure Appl. Algebra, 220, 3207--3232.
  • Rinaldi, D., Schuster, P., & Wessel, D. (2017). Eliminating disjunctions by disjunction elimination.
  • 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
  • Schrijvers, T., Oliveira, B., Wadler, P., & Marntirosian, K. (). COCHIS: Stable and Coherent Implicits. JOURNAL OF FUNCTIONAL PROGRAMMING.
  • 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.
  • 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.
  • 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 Capability Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management (without OS Support). Technical Appendix including Proofs and Details. Aarhus University.
  • Skorstengaard, L., Devriese, D., & Birkedal, L. (2018). Reasoning About a Machine with Local Capabilities. In Programming Languages and Systems. Springer International Publishing.
  • 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.
  • 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).
  • Soloviev, S. V. & Malakhovski, J. (2018). Automorphisms of types and their applications. In Zapiski POMI (pp. 287--308).
  • 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.
  • 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.
  • Swan, A. W. & Uemura, T. (2019). On Church's Thesis in Cubical Assemblies. arXiv:1905.03014.
  • 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.
  • Swan, A. W. (2018). On dividing by two in constructive mathematics. arXiv:1804.04490.
  • 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. (2017). Some Brouwerian Counterexamples Regarding Nominal Sets in Constructive Set Theory. arXiv:1702.01556.
  • Swierstra, W. & Baanen, T. (2019). A predicate transformer semantics for effects. Proc. ACM Program. Lang., 6(ICFP).
  • Swierstra, W. & Dybjer, P. (2017). Special issue on Programming with Dependent Types Editorial. Journal of Functional Programming, 27, e15.
  • 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).
  • Traytel, D. (2017). Formal Languages, Formally and Coinductively. Logical Methods in Computer Science, 13(3).
  • Vezzosi, A., Mortberg, A., & Abel, A. (2019). Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types. In ICFP.
  • 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.
  • 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).
  • 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.
  • 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.