Automath

Automath is a language designed by N.G. the Bruijn in the late sixties in order to represent mathematical proof in the computer. It’s the direct ancestor of the ”type theoretical” line of proof assistants from which the better known current ones are Nuprl and Coq.


References in zbMATH (referenced in 339 articles , 2 standard articles )

Showing results 1 to 20 of 339.
Sorted by year (citations)

1 2 3 ... 15 16 17 next

  1. Alex A. Alemi, Francois Chollet, Niklas Een, Geoffrey Irving, Christian Szegedy, Josef Urban: DeepMath - Deep Sequence Models for Premise Selection (2018) arXiv
  2. Bancerek, Grzegorz; Byliński, Czesław; Grabowski, Adam; Korniłowicz, Artur; Matuszewski, Roman; Naumowicz, Adam; Pąk, Karol: The role of the Mizar mathematical library for interactive proof development in Mizar (2018)
  3. Bendkowski, Maciej; Grygiel, Katarzyna; Tarau, Paul: Random generation of closed simply typed (\lambda)-terms: a synergy between logic programming and Boltzmann samplers (2018)
  4. Coquand, Thierry: Combinatorial topology and constructive mathematics (2018)
  5. Fujita, Ken-etsu: The Church-Rosser theorem and quantitative analysis of witnesses (2018)
  6. Grayson, Daniel R.: An introduction to univalent foundations for mathematicians (2018)
  7. Kremer, Philip: Completeness of second-order propositional S4 and H in topological semantics (2018)
  8. Pistone, Paolo: Polymorphism and the obstinate circularity of second order logic: a victims’ tale (2018)
  9. Rossberg, Andreas: 1ML -- core and modules united (2018)
  10. Stump, Aaron: From realizability to induction via dependent intersection (2018)
  11. Arrighi, Pablo; Díaz-Caro, Alejandro; Valiron, Benoît: The vectorial (\lambda)-calculus (2017)
  12. Berger, Ulrich; Hou, Tie: A realizability interpretation of Church’s simple theory of types (2017)
  13. Coquand, Thierry: Type theory and formalisation of mathematics (2017)
  14. Honsell, Furio; Liquori, Luigi; Maksimovic, Petar; Scagnetto, Ivan: (\mathsfLLF_\mathcalP): a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads (2017)
  15. Kosterec, Miloš: On the number of types (2017)
  16. Blanqui, Frédéric: Termination of rewrite relations on (\lambda)-terms based on Girard’s notion of reducibility (2016)
  17. Chatzikyriakidis, Stergios; Luo, Zhaohui: Proof assistants for natural language semantics (2016)
  18. Kamareddine, Fairouz; Seldin, Jonathan P.; Wells, J. B.: Bridging curry and Church’s typing style (2016)
  19. Yang, Yanpeng; Bi, Xuan; Oliveira, Bruno C.d. S.: Unified syntax with iso-types (2016)
  20. Alves, S.; Broda, S.: A short note on type-inhabitation: formula-trees vs. game semantics (2015)

1 2 3 ... 15 16 17 next