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.
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
Monday, 2 May, 2016, 1-2PM, Swain West 217
Reading: "On Sense and Reference" by Gottlob Frege. Jason got a copy through ILL and put it here.
Presenting: Jason Hemann
Monday, 25 April, 2016, 1-2PM, Swain West 217
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.
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)
Calculus of (Inductive) Constructions
Observational Type Theory
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.