Abstract is missing.
- Counting Environments and ClosuresMaciej Bendkowski, Pierre Lescanne. [doi]
- Analysing Privacy-Type Properties in Cryptographic Protocols (Invited Talk)Stéphanie Delaune. [doi]
- Higher-Order Equational Pattern Anti-UnificationDavid M. Cerna, Temur Kutsia. [doi]
- Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting SystemsNaoki Nishida 0001, Yuya Maeda. [doi]
- Term-Graph Anti-UnificationAlexander Baumgartner, Temur Kutsia, Jordi Levy, Mateu Villaret. [doi]
- Cumulative Inductive Types In CoqAmin Timany, Matthieu Sozeau. [doi]
- ProTeM: A Proof Term Manipulator (System Description)Christina Kohl, Aart Middeldorp. [doi]
- Index-Stratified TypesRohan Jacob-Rao, Brigitte Pientka, David Thibodeau. [doi]
- Homogeneity Without Loss of GeneralityPawel Parys. [doi]
- Lifting Coalgebra Modalities and IMELL Model Structure to Eilenberg-Moore CategoriesJean-Simon Pacaud Lemay. [doi]
- The Clocks They Are Adjunctions Denotational Semantics for Clocked Type TheoryBassel Mannaa, Rasmus Ejlers Møgelberg. [doi]
- On Repetitive Right Application of B-TermsMirai Ikebuchi, Keisuke Nakano. [doi]
- Strict Ideal Completions of the Lambda CalculusPatrick Bahr. [doi]
- Proof Techniques for Program Equivalence in Probabilistic Higher-Order Languages (Invited Talk)Valeria Vignudelli. [doi]
- A Unifying Framework for Type InhabitationSandra Alves, Sabine Broda. [doi]
- Proof Nets for Bi-Intuitionistic Linear LogicGianluigi Bellin, Willem Heijltjes. [doi]
- Confluence of Prefix-Constrained Rewrite SystemsNirina Andrianarivelo, Pierre Réty. [doi]
- Fixed-Point Constraints for Nominal Equational UnificationMauricio Ayala-Rincón, Maribel Fernández, Daniele Nantes Sobrinho. [doi]
- Front Matter, Table of Contents, Preface, Conference Organization [doi]
- Call-by-Name Gradual Type TheoryMax S. New, Daniel R. Licata. [doi]
- Internal Universes in Models of Homotopy Type TheoryDaniel R. Licata, Ian Orton, Andrew M. Pitts, Bas Spitters. [doi]
- Completeness of Tree Automata CompletionThomas Genet. [doi]
- Challenges in Quantum Programming Languages (Invited Talk)Peter Selinger. [doi]
- A Syntax for Higher Inductive-Inductive TypesAmbrus Kaposi, András Kovács. [doi]
- Completion for Logically Constrained RewritingSarah Winkler, Aart Middeldorp. [doi]
- Term Rewriting Characterisation of LOGSPACE for Finite and Infinite DataLukasz Czajka 0001. [doi]
- A Diagrammatic Axiomatisation of Fermionic Quantum CircuitsAmar Hadzihasanovic, Giovanni de Felice, Kang Feng Ng. [doi]
- Confluence Competition 2018Takahito Aoto 0001, Makoto Hamana, Nao Hirokawa, Aart Middeldorp, Julian Nagele, Naoki Nishida 0001, Kiraku Shintani, Harald Zankl. [doi]
- Nominal Unification with Atom and Context VariablesManfred Schmidt-Schauß, David Sabel. [doi]
- Unique perfect matchings and proof netsLê Thành Dung Nguyen. [doi]
- Coherence of Gray Categories via RewritingSimon Forest, Samuel Mimram. [doi]
- Formal Design, Implementation and Verification of Blockchain Languages (Invited Talk)Grigore Rosu. [doi]
- Decreasing Diagrams with Two Labels Are Complete for Confluence of Countable SystemsJörg Endrullis, Jan Willem Klop, Roy Overbeek. [doi]