Pages that link to "Item:Q3793765"

The following pages link to Generalizing Automath by means of a lambda-typed lambda calculus (Q3793765):

Displaying 22 items.

• A prismoid framework for languages with resources (Q654907) (← links)
• A typed \(\lambda\)-calculus for proving-by-example and bottom-up generalization procedure (Q674399) (← links)
• Using typed lambda calculus to implement formal systems on a machine (Q688571) (← links)
• Telescopic mappings in typed lambda calculus (Q757027) (← links)
• Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations (Q853738) (← links)
• Uniformity and the Taylor expansion of ordinary lambda-terms (Q944386) (← links)
• Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms (Q964000) (← links)
• A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction (Q1075050) (← links)
• The calculus of constructions (Q1108266) (← links)
• General recursive functions in a very simply interpretable typed \(\lambda\)-calculus (Q1314352) (← links)
• Selected papers on AUTOMATH, dedicated to N. G. de Bruijn (Q1340050) (← links)
• A useful \(\lambda\)-notation (Q1365680) (← links)
• Higher-order substitutions (Q1854398) (← links)
• A new implementation of Automath (Q1868514) (← links)
• The differential lambda-calculus (Q1884894) (← links)
• A higher-order calculus and theory abstraction (Q2639838) (← links)
• A plea for weaker frameworks (Q4012875) (← links)
• An introduction to differential linear logic: proof-nets, models and antiderivatives (Q4577980) (← links)
• Tactics and Parameters (Q4924546) (← links)
• (Q5140267) (← links)
• On extensibility of proof checkers (Q6061878) (← links)
• The Alf proof editor and its proof engine (Q6083695) (← links)