The group will meet weekly, also during the summers, for a period of one hour. Everyone has the responsibility to read the material before arriving, but one person will have the responsibility of being in solid command of it and presenting it as a discussion starter.
Tori/Vikraman is responsible for booking rooms and taking care of the administrative work.
Tuesdays 12-1PM, Luddy Hall 3069
- Locally cartesian closed categories and type theory by R. A. G. Seely
- Compiling to Categories (contd.)
- Compiling to Categories (contd.)
- Compiling to Categories by Conal Elliott
- Paper website
- CANCELLED (everyone’s sick)
- Planning meeting
- Tori Lewis
- Ramified Recurrence with Dependent Types by Norman Danner
- Un-paywalled link
- Hamidreza Bahramian
- Copredication in homotopy type theory by Hamidreza Bahramian, Narges Nematollahi, and Amr Sabry
- No meeting
- Ryan Scott presenting AND organizing
- Safe Zero-cost Coercions for Haskell by Breitner, Eisenberg, Peyton Jones, and Weirich
- No meeting
- Tori Lewis
- A Finite Axiomatization of Inductive-Recursive Definitions by Dybjer and Setzer
- David Christiansen
- The Gentle Art of Levitation by Chapman, Dagand, McBride, and Morris
- Chao-Hong Chen
- Tori Lewis
- David Christiansen
- Interactive Programs in Dependent Type Theory by Peter Hancock and Anton Setzer
- Vikraman Choudhury
- Appendix B from Guillaume Brunerie’s thesis: The cardinal of π₄(𝕊³)
- Ryan Scott
- Presenting Chapter 4 from Richard Eisenberg’s thesis (pp 51–66)
- US Labor Day and ICFP, no meeting
- Planning meeting in THE ABYSS
- David Christiansen
- On the Degeneracy of Σ-Types in Presence of Computational Classical Logic by Hugo Herbelin
- No meeting
- Chao-Hong Chen
- The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation by Martín Escardó and Chuangjie Xu
- Vikraman Choudhury
- Canonicity for 2-Dimensional Type Theory by Dan Licata and Bob Harper
- David Christiansen
- Epigram Reloaded: A Standalone Typechecker for ETT by James Chapman, Thorsten Altenkirch, and Conor McBride
- Tori Lewis
- A Nominal Exploration of Intuitionism by Vincent Rahli and Mark Bickford
- No meeting, Spring Break
- Robert Rose
- The Groupoid Interpretation of Type Theory by Martin Hofmann and Thomas Streicher (continuing from last week)
- Robert Rose
- The Groupoid Interpretation of Type Theory by Martin Hofmann and Thomas Streicher
- Weixi Ma
- Combining testing and proving in dependent type theory by Peter Dybjer, Qiao Haiyan, and Makoto Takeyama
- David Christiansen
- Algebraic Foundations of Proof Refinement by Jonathan Sterling and Robert Harper
- Kyle Carter
- Stack Semantics of Type Theory by Thierry Coquand, Bassel Mannaa, and Fabian Ruch
- Planning meeting
- Decision: we stick to Mondays at 11
- No meeting due to winter break.
- Control operators and types pt 2
- Reading: http://www.cs.indiana.edu/~sabry/papers/contFoundationLong.pdf
- Presenting: Amr Sabry
- Finals week.
- Contextual Isomorphisms
- https://www.cs.bham.ac.uk/~pbl/papers/contextiso.pdf
- Presenting: Vikraman Choudhury
- Control operators and types pt 1
- http://www.cs.indiana.edu/~sabry/papers/foundationAbortive-TR.pdf esp. sections 1-3
- Presenting: Amr Sabry
- Agda code from talk
- US Thanksgiving week, so no meeting.
- “Löb’s Theorem: A functional pearl of dependently typed quining” by Jason Gross, Jack Gallagher, and Benya Fallenstein.
- https://jasongross.github.io/lob-paper/nightly/lob.pdf
- Presenting: Weixi Ma
- Planning meeting.
- “Truth of a proposition, evidence of a judgement, validity of a proof” by Per Martin-Löf. Synthese 73(3), pp. 407–420. 1987.
- https://michaelt.github.io/martin-lof/Truth-of-a-Proposition-Evidence-of-a-Judgment-1987.pdf
- Presenting: David Christiansen
- “Observational Equality, Now!” by Thorsten Altenkirch, Conor McBride, and Wouter Swierstra.
- http://www.cs.nott.ac.uk/~psztxa/publ/obseqnow.pdf
- Presenting: David Christiansen
- No reading. Instead, we will have a discussion session on formalizing category theory, lead by Tang Jiawei.
- Reading: “Denotation of Contextual Modal Type Theory (CMTT): syntax and metaprogramming” by Murdoch J. Gabbay and Aleksandar Nanevski
- Available from author
- Presenting: Kyle Carter
- Reading: “Unifiers as equivalences: proof-relevant unification of dependently typed data” by Cockx, Devriese, and Piessens
- Available on ACM DL
- Presenting: David Christiansen
- Reading: “Constructing Type Systems over an Operational Semantics” by Bob Harper.
- Presenting: Tori Lewis
- Cancelled due to illness
- U.S. Labor Day. No meeting.
- Talk by Edwin Brady. No reading.
- Reading: “The Power of Pi” by Nicolas Oury and Wouter Swierstra
- Presenting: Chaitainya Koparkar
- Reading: “Continuity of Gödel’s system T definable functionals via effectful forcing” by Martín Escardó
- Presenting: Jon Sterling
- Reading: “Homotopy theoretic models of identity types” by Steve Awodey and Michael A. Warren.
- Presenting: Hamidreza Bahramian
- Cancelled
- Reading: “Computational Higher-Dimensional Type Theory” by Carlo Angiuli, Robert Harper, and Todd Wilson.
- Presenting: David Christiansen
- Reading: “Cubical Type Theory: a constructive interpretation of the univalence axiom” by Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg
- Presenting: Tim Zakian
- Reading: “Ornamental Algebras, Algebraic Ornaments” by Conor McBride.
- Presenting: Jason Hemann
- Change of venue: LH 325
Cancelled due to U.S. Independence Day.
- Reading: “Outrageous but Meaningful Coincidences” by Conor McBride.
- Presenting: Kyle Carter
- Reading: “Idris, a General Purpose Dependently Typed Programming Language: Design and Implementation” by Edwin Brady. In Journal of Functional Programming, October 2013.
- Presenting: Rajan Walia
- Reading: “Indexed Containers” by Thorsten Altenkirch, Neil Ghani, Peter Hancock, Conor McBride, and Peter Morris. In LICS 2009.
- Presenting: Larry Moss
- Reading: “Pattern matching with dependent types” by Thierry Coquand. From a 1992 workshop at Båstad.
- Presenting: Andrew Kent
Cancelled due to Memorial Day.
Cancelled.
- Reading: “A Non-Type-Theoretic Definition of Martin-Löf’s Types” by Stuart Allen. Available from Cornell. We should read the “Reset for better legibility” version of the tech report.
- Presenting: Tori Lewis
- Reading: “Constructive Mathematics and Computer Programming” by Per Martin-Löf. A high-quality reprint of it is available from The Royal Society (works on-campus, at least).
- Presenting: Dan Friedman
- Reading: “On Sense and Reference” by Gottlob Frege. Jason got a copy through ILL and put it here.
- Presenting: Jason Hemann
- Reading: “Program Testing and The Meaning Explanations of Martin-Löf Type Theory” by Peter Dybjer. Chapter 11 of Epistemology versus Ontology, Essays on the Philosophy and Foundations of Mathematics in Honour of Per Martin-Löf, 2012. Available from the author’s Web site and, on campus, through SpringerLink.
- Presenting: David Christiansen
- Reading: “Intuitionistic Type Theory” (the Bibliopolis book) by Per Martin-Löf. Available online from Johan Granström’s page.
- Presenting: David Christiansen
- Gottlob Frege. On Sense and Reference (Über Sinn und Bedeutung)
- Dana Scott. Constructive Validity. In Symposium on Automatic Demonstration, Volume 125 of the series Lecture Notes in Mathematics, pp. 237-275. Springer.
- An intuitionistic theory of types: Predicative part. In H. E. Rose and J. C. Shepherdson, editors, Logic Colloquium ‘73, pages 73–118. North Holland, 1975.
- Constructive mathematics and computer programming. In Logic, Methodology and Philosophy of Science VI, 1979. Eds. Cohen, et al. North-Holland, Amsterdam. pp. 153–175, 1982.
- Intuitionistic type theory (the Bibliopolis book)
- On the Meanings of the Logical Constants and the Justification of Logical Laws (lecture notes from 1983, printed in Nordic Journal of Philosophical Logic in 1996)
- Truth of a proposition, evidence of a judgement, validity of a proof. Synthese 73(3), pp. 407–420. 1987.
- Hofmann and Streicher. The Groupoid Interpretation of Type Theory. (in “25 Years of Constructive Type Theory” or available from Streicher’s Web page)
- Mendler, Nax. Inductive Definition in Type Theory. PhD thesis, Cornell, 1988.
- Peter Dybjer. Inductive Families, in Formal Aspects of Computing 6, 1994
- Peter Dybjer. A general formulation of simultaneous inductive-recursive definitions in type theory, Journal of Symbolic Logic, Volume 65, Number 2, June 2000, pp 525-549
- Peter Dybjer and Anton Setzer. A finite axiomatization of inductive-recursive definitions. Pages 129 - 146 in Proceedings of TLCA 1999, LNCS 1581.
- James Chapman, Pierre-Évariste Dagand, Conor McBride, Peter Morris. The Gentle Art of Levitation. ICFP 2010.
- Guarded Dependent Type Theory with Coinductive Types by Aleš Bizjak, Hans Bugge Grathwohl, Ranald Clouston, Rasmus E. Møgelberg, and Lars Birkedal.
- Guarded Cubical Type Theory: Path Equality for Guarded Recursion by Lars Birkedal, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, and Andrea Vezzosi https://arxiv.org/pdf/1606.05223.pdf
- Non-wellfounded trees in Homotopy Type Theory by Benedikt Ahrens, Paolo Capriotti, Régis Spadotti https://arxiv.org/pdf/1504.02949.pdf
- Peter Dybjer. Program Testing and The Meaning Explanations of Martin-Löf Type Theory. Epistemology versus Ontology, Essays on the Philosophy and Foundations of Mathematics in Honour of Per Martin-Löf, 2012.
- Anton Setzer: Coalgebras as Types determined by their Elimination Rules (in same book)
- N. G. de Bruijn. Telescopic Mappings in Typed Lambda Calculus. Information and Computation 91, pp. 189–204 (1991).
- Robert Harper and Robert Pollack. Type Checking with Universes.
- Pattern Matching with Dependent Types. Thierry Coquand, Proc. of 1992 Workshop on Types for Proofs and Programs in Båstad.
- Pattern Matching Without K. Jesper Cockx, Dominique Devriese, and Frank Piessens. Proceedings of ICFP 2014.
- Edwin Brady. Idris, a General Purpose Dependently Typed Programming Language: Design and Implementation. JFP, October 2013.
- Robert Constable. Naive Computational Type Theory. Proof and System-Reliability, H. Schwichtenberg and R. Steinbruggen (eds.), pp. 213-259.
- Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian E. Aydemir, Eli Barzilay, Yegor Bryukhov, Richard Eaton, Adam Granicz, Alexei Kopylov, Christoph Kreitz, Vladimir N. Krupski, Lori Lorigo, Stephan Schmitt, Carl Witty, and Xin Yu. MetaPRL - A Modular Logical Environment. TPHOLS 2003.
- The View From the Left (initial version)
- The View From the Left (published version)
- Thorsten Altenkirch and Conor McBride and Wouter Swierstra. Observational Equality, Now!. PLPV 2007.
- Casinghino, Sjöberg, and Weirich. Combining Proofs and Programs in a Dependently Typed Language. POPL ‘14.
- CCHM
- CHiTT
- Guarded Cubical
- Higher order unification - implementation