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

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).
  • 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.
  • 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).
  • 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
  • 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).
  • 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).
  • 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).
  • 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.
  • 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.
  • 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).
  • 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
  • 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.
  • 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.
  • 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).
  • 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
  • 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
  • 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).
  • 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.
  • 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..
  • 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).
  • 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.
  • 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.
  • 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).
  • 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).
  • 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).
  • 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.
  • 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 FoSSaCS 2018.
  • 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).
  • 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.
  • 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.
  • 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).
  • 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.
  • 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. (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.
  • 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.
  • 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).
  • 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.
  • 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.
  • 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
  • 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., 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.
  • 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).
  • 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.
  • 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).
  • 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).
  • 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

  • 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.
  • 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.
  • 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
  • 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
  • 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).
  • 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.
  • 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.
  • Dinsdale-Young, T., Spitters, B., Thompson, S. E., & Tschudi, D. (2019). WIP: Formalizing the Concordium consensus protocol in Coq.
  • Eremondi, J., Swierstra, W., & Hage, J. (2019). A framework for improving error messages in dependently-typed languages. Open Computer Science, 9, 1-32.
  • Faggian, C. & Rocca, S. R. D. (2019). Lambda Calculus and Probabilistic Computation. CoRR, abs/1901.02853.
  • 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
  • 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.
  • Gratzer, D., Sterling, J., & Birkedal, L. (2019). Implementing a Modal Dependent Type Theory.
  • 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.
  • Kavvos, G. A. (2019). Modalities, Cohesion, and Information Flow. Proceedings of the ACM on Programming Languages, 3(POPL).
  • 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.
  • 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.
  • 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. (2019). From mathematical axioms to mathematical rules of proof: recent developments in proof analysis. Philosophical Transactions of the Royal Society A, 377(2140), 20180037.
  • Orlova, N. & Soloviev, S. (2019). Logic and logicians in Russia before 1917: Living in a wider world. Historia Mathematica, 46, 38-55.
  • 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.
  • 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.
  • 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
  • Skorstengaard, L., Devriese, D., & Birkedal, L. (2019). StkTokens: enforcing well-bracketed control flow and stack encapsulation using linear capabilities. PACMPL, 3(POPL), 19:1--19:28.
  • Soloviev, S. (2019). Automorphisms of Types in Certain Type Theories and Representation of Finite Groups. Mathematical Structures in Computer Science, 29(4), 511--551.
  • 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).
  • 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.