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

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

1 2 3 ... 19 20 21 next

  1. Carette, Jacques; Farmer, William M.; Kohlhase, Michael; Rabe, Florian: Big math and the one-brain barrier: the tetrapod model of mathematical knowledge (2021)
  2. Abel, Andreas; Coquand, Thierry: Failure of normalization in impredicative type theory with proof-irrelevant propositional equality (2020)
  3. Bry, François: In praise of impredicativity: a contribution to the formalization of meta-programming (2020)
  4. Di Pierro, Alessandra: A type theory for probabilistic (\lambda)-calculus (2020)
  5. Kosterec, Miloš: Substitution contradiction, its resolution and the Church-Rosser theorem in TIL (2020)
  6. Polonsky, Andrew: Fixed point combinators as fixed points of higher-order fixed point generators (2020)
  7. Quaresma, Pedro: Automated deduction and knowledge management in geometry (2020)
  8. Quaresma, Pedro; Santos, Vanda; Graziani, Pierluigi; Baeta, Nuno: Taxonomies of geometric problems (2020)
  9. Tarau, Paul: Deriving efficient sequential and parallel generators for closed simply-typed lambda terms and normal forms (2020)
  10. Weber, Matthias: An extended type system with lambda-typed lambda-expressions (2020)
  11. Hill, Brian; Poggiolesi, Francesca: An analytic calculus for the intuitionistic logic of proofs (2019)
  12. Holliday, Wesley H.: A note on algebraic semantics for (\mathsfS5) with propositional quantifiers (2019)
  13. Libal, Tomer; Volpe, Marco: A general proof certification framework for modal logic (2019)
  14. Alex A. Alemi, Francois Chollet, Niklas Een, Geoffrey Irving, Christian Szegedy, Josef Urban: DeepMath - Deep Sequence Models for Premise Selection (2018) arXiv
  15. 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)
  16. Bendkowski, Maciej; Grygiel, Katarzyna; Tarau, Paul: Random generation of closed simply typed (\lambda)-terms: a synergy between logic programming and Boltzmann samplers (2018)
  17. Blanqui, Frédéric: Size-based termination of higher-order rewriting (2018)
  18. Coquand, Thierry: Combinatorial topology and constructive mathematics (2018)
  19. Ehrhard, Thomas: An introduction to differential linear logic: proof-nets, models and antiderivatives (2018)
  20. Fujita, Ken-etsu: The Church-Rosser theorem and quantitative analysis of witnesses (2018)

1 2 3 ... 19 20 21 next