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

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

1 2 3 ... 14 15 16 next

  1. Arrighi, Pablo; Díaz-Caro, Alejandro; Valiron, Beno^ıt: The vectorial $\lambda$-calculus (2017)
  2. Berger, Ulrich; Hou, Tie: A realizability interpretation of Church’s simple theory of types (2017)
  3. Coquand, Thierry: Type theory and formalisation of mathematics (2017)
  4. 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)
  5. Blanqui, Frédéric: Termination of rewrite relations on $\lambda$-terms based on Girard’s notion of reducibility (2016)
  6. Chatzikyriakidis, Stergios; Luo, Zhaohui: Proof assistants for natural language semantics (2016)
  7. Kamareddine, Fairouz; Seldin, Jonathan P.; Wells, J.B.: Bridging curry and Church’s typing style (2016)
  8. Yang, Yanpeng; Bi, Xuan; Oliveira, Bruno C.d.S.: Unified syntax with iso-types (2016)
  9. Alves, S.; Broda, S.: A short note on type-inhabitation: formula-trees vs. game semantics (2015)
  10. Blanqui, Frédéric; Jouannaud, Jean-Pierre; Rubio, Albert: The computability path ordering (2015)
  11. Fridlender, Daniel; Pagano, Miguel: Pure type systems with explicit substitutions (2015)
  12. Tarau, Paul: Ranking/unranking of lambda terms with compressed de Bruijn indices (2015)
  13. van der Hoeven, Joris: Towards semantic mathematical editing (2015)
  14. Constable, Robert; Bickford, Mark: Intuitionistic completeness of first-order logic (2014)
  15. Endrullis, Joerg; Hendriks, Dimitri; Klop, Jan Willem; Polonsky, Andrew: Discriminating lambda-terms using clocked Böhm trees (2014)
  16. Hindley, J. Roger: Book review of: H. Barendregt (ed.) et al., Lambda calculus with types (2014)
  17. Lasson, Marc: Canonicity of weak $\omega$-groupoid laws using parametricity theory (2014)
  18. Park, Jonghyun; Seo, Jeongbong; Park, Sungwoo; Lee, Gyesik: Mechanizing metatheory without typing contexts (2014)
  19. Abramsky, Samson: Relational hidden variables and non-locality (2013)
  20. de Vrijer, Roel: In memoriam: Nicolaas Govert de Bruijn (1918--2012). Mathematics and language: the Automath project (2013)

1 2 3 ... 14 15 16 next