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

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

1 2 3 ... 14 15 16 next

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

1 2 3 ... 14 15 16 next