Automath and Pure Type Systems

DOI10.1016/S1571-0661(04)80756-4zbMath1264.03043MaRDI QIDQ4924545

Fairouz Kamareddine, Twan Laan, Rob Nederpelt

Publication date: 6 June 2013

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

A prismoid framework for languages with resources, Automath

Uses Software

• Coq
• Nuprl

Cites Work

• On \(\Pi\)-conversion in the \(\lambda\)-cube and the combination with abbreviations
• Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
• A useful \(\lambda\)-notation
• Revisiting the notion of function
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item