Uh oh!
There was an error while loading. Please reload this page.
- Notifications
You must be signed in to change notification settings - Fork 6
Abstracts
Fabian edited this page Sep 22, 2022
·
66 revisions
(in chronological order)
- Andreas Abel, Simply-typed lambda calculus and cartesian closed categories
- Sandro Stucki, Pure Type Systems (PTS)
- Jannis Limperg, The Yoneda Embedding
- Joel Sjögren, A graphical calculus interpreting lambda-calculus
- Ulf Norell, A case study in dependently typed programming
- Ayberk Tosun, Classical proofs as programs
- Frederik Folkmar Ramcke, Theorems for free
- Nachiappan Valliappan, Normalization for typed lambda calculus with co-products
- Andrea Vezzosi, Parametricity for Dependent Types
- Sandro Stucki, Coeffects and Comonads
- Karin Wibergh, RefactorAgda — refactoring Agda code
- Jannis Limperg, Proof by Reflection
- Frederik Folkmar Ramcke, Kripke-style semantics for simply typed lambda calculus
- Mattias Granberg Olsson, Fix-point theories in first order logic
- Sandro Stucki, Internalizing variance using 2-categories
- Ayberk Tosun, Seemingly impossible functional programs
- Ayberk Tosun, Introduction to Domain Theory with Agda
- Joel Sjögren, The logic of linear equations, electrical resistance, and statistical noise
- Jannis Limperg, Introduction to Homotopy Type Theory
- Jesper Cockx, How to Tame Your Rewrite Rules
- Nachiappan Valliappan, Fine Structure of Linear Logic
- Carlos Tomé Cortiñas, Normalization by evaluation for a monadic language with subtyping
- Jesper Cockx, How to formalize stuff in Agda
- Sandro Stucki, Moggi's Computational Lambda Calculus and Monads
- Sandro Stucki, Gray-Box Monitoring of Hyperproperties
- Abraham Wolk, Constructive Mathematics and Computer Programming
- Jannis Limperg, A Reflexive Graph Model of Sized Types
- Nachiappan Valliappan, From syntax to semantics and back: Demystifying NbE
- Peter Dybjer, Categories with Families: Unityped, Simply Typed, and Dependently Typed
- Riccardo Zanetti, On the impact of semantics in functional optimizing compilers
- Matthías Páll Gissuarson, Abstract Interpretation
- Joel Sjögren, Kan extensions: the big picture of limits and colimits
- Carlos Tomé Cortiñas, Modalities, Cohesion and Information Flow
- Ana Bove, Partiality and general recursion in type theory
- Nachiappan Valliappan, Categorical Combinators
- Frederik Hanghøj Iversen, Univalent Categories — A formalization of category theory in Cubical Agda
- Alexander Fuhs, Verified Compilation to Intrinsically Typed Control-Flow Graphs in Agda
- Andreas Abel and Sandro Stucki, Simply-Typed λ-Calculus and Cartesian Closed Categories
- David Sands, Improvement Theory
- Thierry Coquand, Some Remarks about Impredicativity
- Inari Listenmaa, Grammatical Framework and Subtyping in GF
- Sandro Stucki, Subtyping and Bidirectional Type Checking in STLC
- Warrick Macmillan, Type Theory and Natural Language Semantics
- Carlos Tomé Cortiñas, Notions of Computation and Monads
- Andreas Abel, Call-By-Push-Value
- Sandro Stucki, Coeffects by Example
- Vikraman Choudhury, Recovering Purity with Comonads and Capabilities
- Andreas Abel, From Normalization by Evaluation to Call-By-Push-Value
- Carlos Tomé and Nachiappan Valliappan, Modal λ-Calculi: Fitch vs. Dual-Context Style
- Jean-Philippe Bernardy, A Unified View of Modalities in Type Systems
- Tjeerd Fokkens, Dag Prawitz's proof of Takeuti's conjecture
- Wolfgang Ahrendt, Dynamic Logic: Principles and Applications
- Andreas Abel, Logical Relations
- Andreas Abel, Parametricity
- Warrick Macmillan, Modeling Programming Languages in Grammatical Framework
- Warrick Macmillan, On the Grammar of Proof
- Sandro Stucki and Andreas Abel, Simply-Typed λ-Calculus and Cartesian Closed Categories
- Nachiappan Valliappan, Reduction-based Normalization
- Carlos Tomé Cortiñas, Normalization-by-Evaluation by Example
- Andreas Abel, On Consistency, Models, and Normalization for IPL
- Thierry Coquand, Canonicity and normalisation for dependent type theory
- Szumi Xie, Quotient inductive-inductive types
- Peter Dybjer, Martin-Löf's Meaning Explanations for Intuitionistic Type Theory
- Matthew Daggit, Interfacing neural network verifiers with interactive theorem provers