Pages that link to "Item:Q1340050"

The following pages link to Selected papers on AUTOMATH, dedicated to N. G. de Bruijn (Q1340050):

Displaying 48 items.

• Electronic communication of mathematics and the interaction of computer algebra systems and proof assistants (Q597106) (← links)
• Obituary: Nicolaas Govert de Bruijn (1918--2012). Mathematician, computer scientist, logician (Q740456) (← links)
• N. G. de Bruijn's contribution to the formalization of mathematics (Q740481) (← links)
• De Bruijn's weak diamond property revisited (Q740482) (← links)
• Isomorphism is equality (Q740487) (← links)
• SAD as a mathematical assistant -- how should we go from here to there? (Q865654) (← links)
• Supporting the formal verification of mathematical texts (Q865656) (← links)
• Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics (Q865658) (← links)
• The seven virtues of simple type theory (Q946569) (← links)
• Proof assistants: history, ideas and future (Q1040001) (← links)
• From constructivism to computer science (Q1274450) (← links)
• Perpetual reductions in \(\lambda\)-calculus (Q1286373) (← links)
• On \(\Pi\)-conversion in the \(\lambda\)-cube and the combination with abbreviations (Q1302298) (← links)
• A unified approach to type theory through a refined \(\lambda\)-calculus (Q1349674) (← links)
• A useful \(\lambda\)-notation (Q1365680) (← links)
• Revisiting the notion of function (Q1394989) (← links)
• De Bruijn's syntax and reductional behaviour of \(\lambda\)-terms: the untyped case (Q1764799) (← links)
• Comparing and implementing calculi of explicit substitutions with eta-reduction (Q1779307) (← links)
• Descendants and origins in term rewriting. (Q1854348) (← links)
• A new implementation of Automath (Q1868514) (← links)
• A refinement of de Bruijn's formal language of mathematics (Q1876109) (← links)
• Automated deduction and knowledge management in geometry (Q1995808) (← links)
• Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL (Q2102946) (← links)
• Taxonomies of geometric problems (Q2334578) (← links)
• On the mechanization of the proof of Hessenberg's theorem in coherent logic (Q2471743) (← links)
• Computerizing mathematical text with MathLang (Q2866734) (← links)
• A logical framework with explicit conversions (Q2871837) (← links)
• The language of formal mathematics Russell (Q2899004) (← links)
• New Developments in Parsing Mizar (Q2907343) (← links)
• Mathematics and computers (Q3478365) (← links)
• Generalizing Automath by means of a lambda-typed lambda calculus (Q3793765) (← links)
• A plea for weaker frameworks (Q4012875) (← links)
• Implicit coercions in type systems (Q4647565) (← links)
• Comparing Calculi of Explicit Substitutions with Eta-reduction (Q4916203) (← links)
• Automath and Pure Type Systems (Q4924545) (← links)
• Combinatory reduction systems with explicit substitution that preserve strong normalisation (Q5055859) (← links)
• Characteristics of de Bruijn’s early proof checker Automath (Q5089679) (← links)
• A Flexible Framework for Visualisation of Computational Properties of General Explicit Substitutions Calculi (Q5179010) (← links)
• Formalization of constructivity in Automath (Q5187278) (← links)
• Introduction to Type Theory (Q5191087) (← links)
• Formalizing Scientifically Applicable Mathematics in a Definitional Framework (Q5195269) (← links)
• A practical implementation of simple consequence relations using inductive definitions (Q5234714) (← links)
• On Correctness of Mathematical Texts from a Logical and Practical Point of View (Q5505538) (← links)
• The practice of logical frameworks (Q5878905) (← links)
• On the role of OpenMath in interactive mathematical documents (Q5950932) (← links)
• An induction principle for pure type systems (Q5958776) (← links)
• Measuring the readability of geometric proofs: the area method case (Q6156633) (← links)
• Set theory, higher order logic or both? (Q6567712) (← links)