Tag: LICS
-
Discussing “A modality for recursion”
The algorithm I use to choose reading for this blog, pulling the most cited papers out of my Google Scholar recommendations of new papers, sometimes pops out work close to my heart; quite a few years of my own research have been direct outshoots from this paper, following its adoption by Birkedal et al., and…
-
Discussing “A Mechanization of the Blakers–Massey Connectivity Theorem in Homotopy Type Theory”
I first became aware of this paper from a long and fascinating blog comment thread in which mathematicians argued about the utility, or lack thereof, of homotopy type theory for homotopy theorists. Urs Schreiber, arguing for team HoTT, held up this paper an exemplar of the value of the type theoretical approach, saying “it was…
Categories
Recent Posts
- Discussing “An algebraic and Kripke-style approach to a certain extension of intuitionistic logic”
- Discussing “A very modal model of a modern, major, general type system”
- Discussing “The MetaCoq Project”
- Discussing “First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory”
Tags
2000 2001 2014 2019 2023 Andrew W. Appel Anupam Das Cambridge Tracts in Theoretical Computer Science Carnegie Mellon University Christopher D. Richards City University of New York Coq Cubical Type Theory Fabian Kunze Guarded recursion Hiroshi Nakano INRIA Rocquencourt intuitionistic logic intuitionistic modal logic Jonathan Sterling LICS LORIA Maarten de Rijke Melvin Fitting modal logic nested sequent calculus Notre Dame Journal of Formal Logic Patrick Blackburn Paul-André Melliès Princeton University Rocq Ryukoku University Saarland University sequent calculus Sonia Marin Studia Logica TABLEAUX types type theory University of Amsterdam University of Birmingham University of Cambridge University of Oxford Université Paris 7 Yde Venema