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

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

1 2 3 ... 13 14 15 next

  1. Blanqui, Frédéric: Termination of rewrite relations on $\lambda$-terms based on Girard’s notion of reducibility (2016)
  2. Kamareddine, Fairouz; Seldin, Jonathan P.; Wells, J.B.: Bridging curry and Church’s typing style (2016)
  3. Alves, S.; Broda, S.: A short note on type-inhabitation: formula-trees vs. game semantics (2015)
  4. Blanqui, Frédéric; Jouannaud, Jean-Pierre; Rubio, Albert: The computability path ordering (2015)
  5. van der Hoeven, Joris: Towards semantic mathematical editing (2015)
  6. Constable, Robert; Bickford, Mark: Intuitionistic completeness of first-order logic (2014)
  7. Endrullis, Joerg; Hendriks, Dimitri; Klop, Jan Willem; Polonsky, Andrew: Discriminating lambda-terms using clocked Böhm trees (2014)
  8. Lasson, Marc: Canonicity of weak $\omega$-groupoid laws using parametricity theory (2014)
  9. Park, Jonghyun; Seo, Jeongbong; Park, Sungwoo; Lee, Gyesik: Mechanizing metatheory without typing contexts (2014)
  10. Abramsky, Samson: Relational hidden variables and non-locality (2013)
  11. de Vrijer, Roel: In memoriam: Nicolaas Govert de Bruijn (1918--2012). Mathematics and language: the Automath project (2013)
  12. Geuvers, Herman; Nederpelt, Rob: N. G. de Bruijn’s contribution to the formalization of mathematics (2013)
  13. Harrison, John: The HOL Light theory of Euclidean space (2013)
  14. Klop, Jan Willem: Obituary: Nicolaas Govert de Bruijn (1918--2012). Mathematician, computer scientist, logician (2013)
  15. Ochs, Eduardo: Internal diagrams and archetypal reasoning in category theory (2013)
  16. Rabe, Florian; Kohlhase, Michael: A scalable module system (2013)
  17. Stirton, William R.: A decidable theory of type assignment (2013)
  18. Stump, Aaron; Kimmell, Garrin; Zantema, Hans; El Haj Omar, Ruba: A rewriting view of simple typing (2013)
  19. Arrighi, Pablo; Díaz-Caro, Alejandro: A System F accounting for scalars (2012)
  20. Asperti, Andrea; Ricciotti, Wilmer; Sacerdoti Coen, Claudio; Tassi, Enrico: A bi-directional refinement algorithm for the calculus of (co)inductive constructions (2012)

1 2 3 ... 13 14 15 next