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

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

1 2 3 ... 14 15 16 next

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

1 2 3 ... 14 15 16 next