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

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

1 2 3 ... 15 16 17 next

  1. 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)
  2. Bendkowski, Maciej; Grygiel, Katarzyna; Tarau, Paul: Random generation of closed simply typed $\lambda$-terms: a synergy between logic programming and Boltzmann samplers (2018)
  3. Grayson, Daniel R.: An introduction to univalent foundations for mathematicians (2018)
  4. Pistone, Paolo: Polymorphism and the obstinate circularity of second order logic: a victims’ tale (2018)
  5. Stump, Aaron: From realizability to induction via dependent intersection (2018)
  6. Arrighi, Pablo; Díaz-Caro, Alejandro; Valiron, Beno^ıt: The vectorial $\lambda$-calculus (2017)
  7. Berger, Ulrich; Hou, Tie: A realizability interpretation of Church’s simple theory of types (2017)
  8. Coquand, Thierry: Type theory and formalisation of mathematics (2017)
  9. Honsell, Furio; Liquori, Luigi; Maksimovic, Petar; Scagnetto, Ivan: $\mathsfLLF_\CalP$: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads (2017)
  10. Kosterec, Miloš: On the number of types (2017)
  11. Blanqui, Frédéric: Termination of rewrite relations on $\lambda$-terms based on Girard’s notion of reducibility (2016)
  12. Chatzikyriakidis, Stergios; Luo, Zhaohui: Proof assistants for natural language semantics (2016)
  13. Kamareddine, Fairouz; Seldin, Jonathan P.; Wells, J. B.: Bridging curry and Church’s typing style (2016)
  14. Yang, Yanpeng; Bi, Xuan; Oliveira, Bruno C.d. S.: Unified syntax with iso-types (2016)
  15. Alves, S.; Broda, S.: A short note on type-inhabitation: formula-trees vs. game semantics (2015)
  16. Blanqui, Frédéric; Jouannaud, Jean-Pierre; Rubio, Albert: The computability path ordering (2015)
  17. Fridlender, Daniel; Pagano, Miguel: Pure type systems with explicit substitutions (2015)
  18. Tarau, Paul: Ranking/unranking of lambda terms with compressed de Bruijn indices (2015)
  19. van der Hoeven, Joris: Towards semantic mathematical editing (2015)
  20. Constable, Robert; Bickford, Mark: Intuitionistic completeness of first-order logic (2014)

1 2 3 ... 15 16 17 next