The following pages link to Automath (Q19182):
Displaying 50 items.
- (Q4536445) (← links)
- Computational logic: its origins and applications (Q4559535) (← links)
- Algorithmic Theories of Problems. A Constructive and a Non-Constructive Approach (Q4565827) (← links)
- On explicit substitutions and names (extended abstract) (Q4571957) (← links)
- Size-based termination of higher-order rewriting (Q4577817) (← links)
- An introduction to differential linear logic: proof-nets, models and antiderivatives (Q4577980) (← links)
- A realizability interpretation of Church's simple theory of types (Q4593235) (← links)
- Random generation of closed simply typed λ-terms: A synergy between logic programming and Boltzmann samplers (Q4603430) (← links)
- 1ML – Core and modules united (Q4625163) (← links)
- POLYMORPHISM AND THE OBSTINATE CIRCULARITY OF SECOND ORDER LOGIC: A VICTIMS’ TALE (Q4637941) (← links)
- On the intuitionistic force of classical search (Extended abstract) (Q4645244) (← links)
- Modular properties of algebraic type systems (Q4645803) (← links)
- The variable containment problem (Q4645807) (← links)
- Third-order matching in the polymorphic lambda calculus (Q4645813) (← links)
- Implicit coercions in type systems (Q4647565) (← links)
- A two-level approach towards lean proof-checking (Q4647567) (← links)
- Context-relative syntactic categories and the formalization of mathematical text (Q4647583) (← links)
- A simple model construction for the Calculus of Constructions (Q4647584) (← links)
- Proof normalization modulo (Q4650285) (← links)
- Definitions by rewriting in the Calculus of Constructions (Q4657751) (← links)
- (Q4664918) (← links)
- (Q4664919) (← links)
- (Q4664921) (← links)
- Closed reduction: explicit substitutions without $\alpha$ -conversion (Q4675772) (← links)
- Correspondence assertions for process synchronization in concurrent communications (Q4676156) (← links)
- (Q4681362) (← links)
- An introduction to univalent foundations for mathematicians (Q4684362) (← links)
- (Q4703134) (← links)
- Some logical and syntactical observations concerning the first-order dependent type system λP (Q4704760) (← links)
- (Q4720069) (← links)
- (Q4736483) (← links)
- (Q4801125) (← links)
- (Q4813221) (← links)
- Soundness of Coercion in the Calculus of Constructions (Q4820474) (← links)
- (Q4823135) (← links)
- (Q4880706) (← links)
- Typed answer set programming lambda calculus theories and correctness of inverse lambda algorithms with respect to them (Q4911148) (← links)
- A Rewriting View of Simple Typing (Q4913767) (← links)
- Hyperformulae, Parallel Deductions and Intersection Types (Q4916178) (← links)
- Comparing Calculi of Explicit Substitutions with Eta-reduction (Q4916203) (← links)
- Studying provability in implicational intuitionistic logic (Q4916206) (← links)
- Typing Correspondence Assertions for Communication Protocols (Q4917053) (← links)
- Cut Elimination in a Class of Sequent Calculi for Pure Type Systems (Q4924532) (← links)
- Tactics and Parameters (Q4924546) (← links)
- Remarks on Isomorphisms of Simple Inductive Types (Q4924549) (← links)
- Intersection Type Systems and Explicit Substitutions Calculi (Q4931603) (← links)
- Monotone (co)inductive types and positive fixed-point types (Q4943545) (← links)
- (Q4944847) (← links)
- (Q4945243) (← links)
- A general method for proving the normalization theorem for first and second order typed λ-calculi (Q4946629) (← links)
