You have Guest access.
Log In
Paul Callaghan, Zhaohui Luo, James McKinna, Robert Pollack and Robert Pollack
Front matter
728
Collection Principles in Dependent Type Theory
725
Executing Higher Order Logic
A Tour with Constructive Real Numbers
727
An Implementation of Type:Type
On the Logical Content of Computational Type Theory: A Solution to Curry’s Problem
725-726
Constructive Reals in Coq: Axioms and Categoricity
726-727
A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals
726
A Kripke-Style Model for the Admissibility of Structural Rules (Extended Abstract)
Towards Limit Computable Mathematics
724
Formalizing the Halting Problem in a Constructive Type Theory
On the Proofs of Some Formally Unprovable Propositions and Prototype Proofs in Type Theory
Changing Data Structures in Type Theory: A Study of Natural Numbers
Elimination with a Motive
Generalization in Type Theory Based Proof Assistants
724-725
An Inductive Version of Nash-Williams’ Minimal-Bad-Sequence Argument for Higman’s Lemma
Back matter
Peter Aczel and Nicola Gambino
Stefan Berghofer and Tobias Nipkow
Alberto Ciaffaglione and Pietro Di Gianantonio
Thierry Coquand and Makoto Takeyama
Matt Fairtlough and Michael Mendler
Herman Geuvers and Milad Niqui
Herman Geuvers, Freek Wiedijk and Jan Zwanenburg
Healfdene Goguen
Susumu Hayashi and Masahiro Nakata
Kristofer Johannisson
Giuseppe Longo
Nicolas Magaud and Yves Bertot
Conor McBride
Olivier Pons
Monika Seisenberger
Frequently asked questions General info on journals and books Send us your feedback Impressum Contact us
© Springer, Part of Springer Science+Business Media Privacy, Disclaimer, Terms & Conditions, and Copyright Info