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 397 articles , 2 standard articles )

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

1 2 3 ... 18 19 20 next

  1. Bry, François: In praise of impredicativity: a contribution to the formalization of meta-programming (2020)
  2. Kosterec, Miloš: Substitution contradiction, its resolution and the Church-Rosser theorem in TIL (2020)
  3. Quaresma, Pedro; Santos, Vanda; Graziani, Pierluigi; Baeta, Nuno: Taxonomies of geometric problems (2020)
  4. Hill, Brian; Poggiolesi, Francesca: An analytic calculus for the intuitionistic logic of proofs (2019)
  5. Holliday, Wesley H.: A note on algebraic semantics for (\mathsfS5) with propositional quantifiers (2019)
  6. Libal, Tomer; Volpe, Marco: A general proof certification framework for modal logic (2019)
  7. Alex A. Alemi, Francois Chollet, Niklas Een, Geoffrey Irving, Christian Szegedy, Josef Urban: DeepMath - Deep Sequence Models for Premise Selection (2018) arXiv
  8. 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)
  9. Bendkowski, Maciej; Grygiel, Katarzyna; Tarau, Paul: Random generation of closed simply typed (\lambda)-terms: a synergy between logic programming and Boltzmann samplers (2018)
  10. Blanqui, Frédéric: Size-based termination of higher-order rewriting (2018)
  11. Coquand, Thierry: Combinatorial topology and constructive mathematics (2018)
  12. Ehrhard, Thomas: An introduction to differential linear logic: proof-nets, models and antiderivatives (2018)
  13. Fujita, Ken-etsu: The Church-Rosser theorem and quantitative analysis of witnesses (2018)
  14. Grayson, Daniel R.: An introduction to univalent foundations for mathematicians (2018)
  15. Klev, Ansten: The concept \textithorseis a concept (2018)
  16. Kremer, Philip: Completeness of second-order propositional S4 and H in topological semantics (2018)
  17. Paulson, Lawrence C.: Computational logic: its origins and applications (2018)
  18. Pistone, Paolo: Polymorphism and the obstinate circularity of second order logic: a victims’ tale (2018)
  19. Rossberg, Andreas: 1ML -- core and modules united (2018)
  20. Stump, Aaron: From realizability to induction via dependent intersection (2018)

1 2 3 ... 18 19 20 next