Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
From MaRDI portal
Publication:1340050
zbMath0822.03009MaRDI QIDQ1340050
No author found.
Publication date: 8 December 1994
Published in: Studies in Logic and the Foundations of Mathematics (Search for Journal in Brave)
Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40) Collections of reprinted articles (00B60)
Related Items
Combinatory reduction systems with explicit substitution that preserve strong normalisation, New Developments in Parsing Mizar, A unified approach to type theory through a refined \(\lambda\)-calculus, A useful \(\lambda\)-notation, SAD as a mathematical assistant -- how should we go from here to there?, Supporting the formal verification of mathematical texts, Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics, Electronic communication of mathematics and the interaction of computer algebra systems and proof assistants, Characteristics of de Bruijn’s early proof checker Automath, Revisiting the notion of function, Measuring the readability of geometric proofs: the area method case, The seven virtues of simple type theory, Implicit coercions in type systems, On the mechanization of the proof of Hessenberg's theorem in coherent logic, Automated deduction and knowledge management in geometry, Comparing Calculi of Explicit Substitutions with Eta-reduction, Automath and Pure Type Systems, De Bruijn's syntax and reductional behaviour of \(\lambda\)-terms: the untyped case, A Flexible Framework for Visualisation of Computational Properties of General Explicit Substitutions Calculi, Comparing and implementing calculi of explicit substitutions with eta-reduction, Introduction to Type Theory, On the role of OpenMath in interactive mathematical documents, An induction principle for pure type systems, Obituary: Nicolaas Govert de Bruijn (1918--2012). Mathematician, computer scientist, logician, N. G. de Bruijn's contribution to the formalization of mathematics, De Bruijn's weak diamond property revisited, Isomorphism is equality, From constructivism to computer science, A practical implementation of simple consequence relations using inductive definitions, Perpetual reductions in \(\lambda\)-calculus, Proof assistants: history, ideas and future, On Correctness of Mathematical Texts from a Logical and Practical Point of View, Taxonomies of geometric problems, On \(\Pi\)-conversion in the \(\lambda\)-cube and the combination with abbreviations, Formalizing Scientifically Applicable Mathematics in a Definitional Framework, Descendants and origins in term rewriting., Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL, Computerizing Mathematical Text with MathLang, A Logical Framework with Explicit Conversions, The practice of logical frameworks
Uses Software
