Document Open Access Logo

Teaching Foundations of Computation and Deduction Through Literate Functional Programming and Type Theory Formalization

Author Gérard Huet

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2016.3.pdf
  • Filesize: 230 kB
  • 2 pages

Document Identifiers

Author Details

Gérard Huet

Cite AsGet BibTex

Gérard Huet. Teaching Foundations of Computation and Deduction Through Literate Functional Programming and Type Theory Formalization. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 3:1-3:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.FSCD.2016.3

Abstract

We describe experiments in teaching fundamental informatics notions around mathematical structures for formal concepts, and effective algorithms to manipulate them. The major themes of lambda-calculus and type theory served as guides for the effective implementation of functional programming languages and higher-order proof assistants, appropriate for reflecting the theoretical material into effective tools to represent constructively the concepts and formally certify the proofs of their properties. Progressively, a literate programming and proving style replaced informal mathematics in the presentation of the material as executable course notes. The talk will evoke the various stages of (in)completion of the corresponding set of notes along the years, and tell how their elaboration proved to be essential to the discovery of fundamental results.
Keywords
  • Foundations
  • Computation
  • Deduction
  • Programming
  • Proofs

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Gérard Huet. Initiation à la logique mathématique. Notes de cours du DEA d'Informatique, Université Paris-Sud, 1977. Google Scholar
  2. Gérard Huet. Démonstration automatique en logique de premier ordre et programmation en clauses de horn. Notes de cours du DEA d'Informatique, Université Paris-Sud, 1978. Google Scholar
  3. Gérard Huet. Confluent reductions: Abstract properties and applications to term rewriting systems. J. ACM, 27,4:797-821, 1980. Google Scholar
  4. Gérard Huet. Deduction and computation. In Manfred Broy, editor, Logic of Programming and Calculi of Discrete Design, pages 305-342. Springer Verlag, 1987. Google Scholar
  5. Gérard Huet. Initiation au λ-calcul. Notes de cours du DEA "Fonctionalité, Structures de Calcul et Programmation, Université Paris VII, 1987. Google Scholar
  6. Gérard Huet. Introduction au λ-calcul pur. In Friedrich Bauer, editor, Logic, Algebra and Computation, pages 153-200. Springer Verlag, 1987. Google Scholar
  7. Gérard Huet. Induction principles formalized in the calculus of constructions. In K. Fuchi and M. Nivat, editors, Programming of Future Generation Computers, pages 205-216. North Holland, 1988. Google Scholar
  8. Gérard Huet. Cartesian closed categories and lambda-calculus. In Gérard Huet, editor, Logical Foundations of Functional Programming, pages 7-23. Addison-Wesley, 1989. Google Scholar
  9. Gérard Huet. The Constructive Engine. In R. Narasimhan, editor, A perspective in Theoretical Computer Science. Commemorative Volume for Gift Siromoney. World Scientific Publishing, 1989. Google Scholar
  10. Gérard Huet. A uniform approach to type theory. In Gérard Huet, editor, Logical Foundations of Functional Programming, pages 337-397. Addison-Wesley, 1989. Google Scholar
  11. Gérard Huet. An analysis of Böhm’s theorem. Theoretical Computer Science, 121:145-167, 1993. Google Scholar
  12. Gérard Huet. Constructive computation theory. Course Notes, DEA Informatique, Mathématiques et Applications, Paris VII, 1987, 1993. URL: http://yquem.inria.fr/~huet/PUBLIC/CCT.pdf.
  13. Gérard Huet. Residual theory in λ-calculus: a formal development. J. Functional Programming, 4,3:371-394, 1994. Google Scholar
  14. Gérard Huet. Initiation à la théorie des catégories. Notes de cours du DEA "Fonctionalité, Structures de Calcul et Programmation, Université Paris VII, 2nd edition, 1987. Google Scholar
  15. Gérard Huet. A complete proof of correctness of the Knuth-Bendix completion algorithm. J. of Computer and System Sciences, 23,1:11-21, I981. Google Scholar
  16. Gérard Huet. Formal structures for computation and deduction. Course Notes, Carnegie-Mellon University, May 1986. URL: http://yquem.inria.fr/~huet/PUBLIC/Formal_Structures.pdf.
  17. Gérard Huet and Derek Oppen. Equations and rewrite rules: a survey. In Ronald Book, editor, Formal Languages: Perspectives and Open Problems, pages 349-405. Academic Press, 1980. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact