The following pages link to (Q5625124):
Displaying 34 items.
- A simple proof of second-order strong normalization with permutative conversions (Q2566069) (← links)
- Inductive types and type constraints in the second-order lambda calculus (Q2639842) (← links)
- On the Convergence of Reduction-based and Model-based Methods in Proof Theory (Q2866742) (← links)
- Lambda-calcul, évaluation paresseuse et mise en mémoire (Q3204440) (← links)
- A Type Theory for Probabilistic $$\lambda $$–calculus (Q3297838) (← links)
- (Q3300787) (← links)
- On Paths-Based Criteria for Polynomial Time Complexity in Proof-Nets (Q3460508) (← links)
- A Constructive Semantic Approach to Cut Elimination in Type Theories with Axioms (Q3540178) (← links)
- Realizability algebras III: some examples (Q4599612) (← links)
- Cogent: uniqueness types and certifying compilation (Q5019022) (← links)
- On the Versatility of Open Logical Relations (Q5041087) (← links)
- Applications of type theory (Q5044747) (← links)
- Higher-order unification with dependent function types (Q5055716) (← links)
- Adding algebraic rewriting to the untyped lambda calculus (extended abstract) (Q5055747) (← links)
- Programming and Proving with Classical Types (Q5055999) (← links)
- (Q5089012) (← links)
- (Q5094128) (← links)
- An extension of system F with subtyping (Q5096247) (← links)
- (Q5101355) (← links)
- Prawitz, Proofs, and Meaning (Q5213604) (← links)
- Program Testing and the Meaning Explanations of Intuitionistic Type Theory (Q5253930) (← links)
- Free Theorems and Runtime Type Representations (Q5262947) (← links)
- Neo-Logicism and Its Logic (Q5871286) (← links)
- Typed equivalence, type assignment, and type containment (Q5881295) (← links)
- Operations on records (Q5887510) (← links)
- Inductively defined types in the Calculus of Constructions (Q5887516) (← links)
- Algebraic types in PER models (Q5887524) (← links)
- Inductive-data-type systems (Q5958292) (← links)
- A Survey of the Proof-Theoretic Foundations of Logic Programming (Q6063891) (← links)
- Choice and independence of premise rules in intuitionistic set theory (Q6109095) (← links)
- Reduction Free Normalisation for a proof irrelevant type of propositions (Q6135773) (← links)
- Formula normalizations in verification (Q6535699) (← links)
- Theoretical computer science: computability, decidability and logic (Q6602262) (← links)
- A direct computational interpretation of second-order arithmetic via update recursion (Q6649499) (← links)
