Jonathan Sterling

Proceedings of the 32nd EACSL Annual Conference on Computer Science Logic, 2024

2023

What should a generic object be?

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2023

Tensorial structure of the lifting doctrine in constructive domain theory.

[BibT_eX]

[DOI]

Frederik Lerbjerg Aagaard

CoRR, 2023

A denotationally-based program logic for higher-order store.

[BibT_eX]

[DOI]

Proceedings of the 39th Conference on the Mathematical Foundations of Programming Semantics, 2023

Free theorems from univalent reference types.

[BibT_eX]

[DOI]

CoRR, 2023

Towards a geometry for syntax.

[BibT_eX]

[DOI]

CoRR, 2023

2022

First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory.

[BibT_eX]

[DOI]

PhD thesis, 2022

A cost-aware logical framework.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2022

A Cubical Language for Bishop Sets.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2022

Controlling unfolding in type theory.

[BibT_eX]

[DOI]

CoRR, 2022

Classifying topoi in synthetic guarded domain theory.

[BibT_eX]

[DOI]

Daniele Palombi

Proceedings of the 38th Conference on the Mathematical Foundations of Programming Semantics, 2022

Denotational semantics of general store and polymorphism.

[BibT_eX]

[DOI]

CoRR, 2022

Reflections on existential types.

[BibT_eX]

[DOI]

CoRR, 2022

Strict universes for Grothendieck topoi.

[BibT_eX]

[DOI]

Michael Shulman

CoRR, 2022

Bilimits in categories of partial maps.

[BibT_eX]

[DOI]

CoRR, 2022

The directed plump ordering.

[BibT_eX]

[DOI]

Michael Shulman

CoRR, 2022

Sheaf Semantics of Termination-Insensitive Noninterference.

[BibT_eX]

[DOI]

Proceedings of the 7th International Conference on Formal Structures for Computation and Deduction, 2022

2021

Higher order functions and Brouwer's thesis.

[BibT_eX]

[DOI]

J. Funct. Program., 2021

Logical Relations as Types: Proof-Relevant Parametricity for Program Modules.

[BibT_eX]

[DOI]

J. ACM, 2021

Normalization for Cubical Type Theory.

[BibT_eX]

[DOI]

Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, 2021

2020

Syntactic categories for dependent type theory: sketching and adequacy.

[BibT_eX]

[DOI]

CoRR, 2020

2019

Implementing a modal dependent type theory.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2019

Algebraic Type Theory and Universe Hierarchies.

[BibT_eX]

[DOI]

CoRR, 2019

Cubical Syntax for Reflection-Free Extensional Equality.

[BibT_eX]

[DOI]

Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction, 2019

2018

Normalization by gluing for free λ-theories.

[BibT_eX]

[DOI]

Bas Spitters

CoRR, 2018

The RedPRL Proof Assistant (Invited Paper).

[BibT_eX]

[DOI]

Evan Cavallo

Kuen-Bang Hou (Favonia)

Proceedings of the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2018

Guarded Computational Type Theory.

[BibT_eX]

[DOI]

Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018

2017

Algebraic Foundations of Proof Refinement.

[BibT_eX]

[DOI]

CoRR, 2017

2016

Syntax and Semantics of Abstract Binding Trees.

[BibT_eX]

[DOI]

Darin Morrison

CoRR, 2016

Primitive Recursive Bars Are Inductive.

[BibT_eX]

[DOI]

CoRR, 2016

2015

Type Theory and its Meaning Explanations.

[BibT_eX]

[DOI]

CoRR, 2015

Remark on the hypothetical judgment.

[BibT_eX]

[DOI]

CoRR, 2015

2014

Dependent Types for Pragmatics.

[BibT_eX]

[DOI]

Darryl McAdams