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

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

1 2 3 ... 19 20 21 next

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

1 2 3 ... 19 20 21 next