Minlog - A Tool for Program Extraction Supporting Algebras and Coalgebras

1. Agda: http://wiki.portal.chalmers.se/agda/

2. Berger, U., Berghofer, S., Letouzey, P., Schwichtenberg, H.: Program extraction from normalization proofs. Studia Logica 82, 27–51 (2006)

   Article  MathSciNet  Google Scholar 

3. Benl, H., Berger, U., Schwichtenberg, H., Seisenberger, M., Zuber, W.: Proof theory at work: Program development in the Minlog system. In: Bibel, W., Schmitt, P.H. (eds.) Automated Deduction. Applied Logic Series, vol. II, pp. 41–71. Kluwer, Dordrecht (1998)

   Google Scholar 

4. Berger, U., Buchholz, W., Schwichtenberg, H.: Refined program extraction from classical proofs. APAL 114, 3–25 (2002)

   MathSciNet  MATH  Google Scholar 

5. Berger, U.: From coinductive proofs to exact real arithmetic. In: Grädel, E., Kahle, R. (eds.) CSL 2009. LNCS, vol. 5771, pp. 132–146. Springer, Heidelberg (2009)

   Chapter  Google Scholar 

6. Berger, U., Eberl, M., Schwichtenberg, H.: Term rewriting for normalization by evaluation. Information and Computation 183, 19–42 (2003)

   Article  MathSciNet  MATH  Google Scholar 

7. Berger, U., Hou, T.: Coinduction for exact real number computation. Theory of Computing Systems 43, 394–409 (2008)

   Article  MathSciNet  MATH  Google Scholar 

8. Berger, U., Schwichtenberg, H.: An inverse of the evaluation functional for typed λ-calculus. In: Vemuri, R. (ed.) Proceedings 6’th Symposium on Logic in Computer Science, LICS 1991, pp. 203–211. IEEE Computer Society Press, Los Alamitos (1991)

   Google Scholar 

9. Bauer, A., Stone, C.A.: RZ: A tool for bringing constructive and computable mathematics closer to programming practice. In: Cooper, S.B., Löwe, B., Sorbi, A. (eds.) CiE 2007. LNCS, vol. 4497, pp. 28–42. Springer, Heidelberg (2007)

   Chapter  Google Scholar 

10. Berger, U., Seisenberger, M.: Proofs, programs, processes. In: Ferreira, F., Löwe, B., Mayordomo, E., Mendes Gomes, L. (eds.) CiE 2010. LNCS, vol. 6158, pp. 39–48. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

11. Ciaffaglione, A., Di Gianantonio, P.: A certified, corecursive implementation of exact real numbers. Theor. Comp. Sci. 351, 39–51 (2006)

    Article  MATH  Google Scholar 

12. Chuang, C.M.: Extraction of Programs for Exact Real Number Computation Using Agda. PhD thesis. Swansea University, Wales (2011)

    Google Scholar 

13. The Coq Proof Assistant, http://coq.inria.fr/

14. Crosilla, L., Seisenberger, M., Schwichtenberg, H.: A Tutorial for Minlog, Version 5.0 (2011)

    Google Scholar 

15. Geuvers, H., Niqui, M., Spitters, B., Wiedijk, F.: Constructive analysis, types and exact real numbers. Math. Struct. Comp. Sci. 17(1), 3–36 (2007)

    Article  MathSciNet  MATH  Google Scholar 

16. Isabelle, http://isabelle.in.tum.de/

17. Kreisel, G.: Interpretation of analysis by means of constructive functionals of finite types. Constructivity in Mathematics, 101–128 (1959)

    Google Scholar 

18. Letouzey, P.: A New Extraction for Coq. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol. 2646, pp. 200–219. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

19. Miller, D.: A logic programming language with lambda–abstraction, function variables and simple unification. Jour. Logic Comput. 2(4), 497–536 (1991)

    Article  Google Scholar 

20. The Minlog System, http://www.minlog-system.de

21. Marcial-Romero, J.R., Escardo, M.H.: Semantics of a sequential language for exact real-number computation. Theor. Comp. Sci. 379(1-2), 120–141 (2007)

    Article  MathSciNet  MATH  Google Scholar 

22. Schwichtenberg, H.: Proof search in minimal logic. In: Buchberger, B., Campbell, J.A. (eds.) AISC 2004. LNCS (LNAI), vol. 3249, pp. 15–25. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

23. Schwichtenberg, H., Wainer, S.S.: Proofs and Computations. Perspectives in Logic. Assoc. Symb. Logic, Cambridge Univ. Press (to appear, 2011)

    Google Scholar 

Download references