Advertisement

Combining Proofs and Programs

  • Stephanie Weirich
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6690)

Abstract

Programming languages based on dependent type theory promise two great advances: flexibility and security. With the type-level computation afforded by dependent types, algorithms can be more generic, as the type system can express flexible interfaces via programming. Likewise, type-level computation can also express data structure invariants, so that programs can be proved correct through type checking. Furthermore, despite these extensions, programmers already know everything. Via the Curry-Howard isomorphism, the language of type-level computation and the verification logic is the programming language itself.

References

  1. [Coh63]
    Cohen, P.J.: The independence of the continuum hypothesis. Proceedings of the National Academy of Sciences of the United States of America 50(6), 1143–1148 (1963)CrossRefzbMATHGoogle Scholar
  2. [Coh64]
    Cohen, P.J.: The independence of the continuum hypothesis II. Proceedings of the National Academy of Sciences of the United States of America 51(1), 105–110 (1964)CrossRefGoogle Scholar
  3. [Fri78]
    Friedman, H.: Classically and intuitionistically provably recursive functions. Higher Set Theory 699, 21–28 (1978)CrossRefzbMATHGoogle Scholar
  4. [Gri90]
    Griffin, T.: A formulae-as-types notion of control. In: Principles of Programming Languages (POPL 1990), pp. 47–58 (1990)Google Scholar
  5. [Kle45]
    Kleene, S.C.: On the interpretation of intuitionistic number theory. Journal of Symbolic Logic 10, 109–124 (1945)CrossRefzbMATHGoogle Scholar
  6. [Kri01]
    Krivine, J.-L.: Typed lambda-calculus in classical Zermelo-Fraenkel set theory. Arch. Math. Log. 40(3), 189–205 (2001)CrossRefzbMATHGoogle Scholar
  7. [Kri03]
    Krivine, J.-L.: Dependent choice, ‘quote’ and the clock. Theor. Comput. Sci. 308(1-3), 259–276 (2003)CrossRefzbMATHGoogle Scholar
  8. [Kri09]
    Krivine, J.-L.: Realizability in classical logic. In: Interactive Models of Computation and Program Behaviour. Panoramas et synthèses, vol. 27, pp. 197–229. Société Mathématique de France (2009)Google Scholar
  9. [Kri10]
    Krivine, J.-L.: Realizability algebras: a program to well order R. CoRR, abs/1005.2395 (2010)Google Scholar
  10. [Miq07]
    Miquel, A.: Classical program extraction in the calculus of constructions. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 313–327. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  11. [Miq10]
    Miquel, A.: Existential witness extraction in classical realizability and via a negative translation. Logical Methods for Computer Science (2010)Google Scholar
  12. [OS08]
    Oliva, P., Streicher, T.: On Krivine’s realizability interpretation of classical second-order arithmetic. Fundam. Inform. 84(2), 207–220 (2008)zbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Stephanie Weirich
    • 1
  1. 1.University of PennsylvaniaPhiladelphiaUSA

Personalised recommendations