scientific article; zbMATH DE number 3349775
From MaRDI portal
Publication:5625124
Cited in
(95)- A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction
- A characterization of F-complete type assignments
- The system \({\mathcal F}\) of variable types, fifteen years later
- The calculus of constructions
- Toposes and intuitionistic theories of types
- On Church's formal theory of functions and functionals. The - calculus: Connections to higher type recursion theory, proof theory, category theory
- Recursion over realizability structures
- Metacircularity in the polymorphic \(\lambda\)-calculus
- Bounded linear logic: A modular approach to polynomial-time computability
- Adding algebraic rewriting to the untyped lambda calculus
- Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi
- Typing untyped \(\lambda\)-terms, or reducibility strikes again!
- Computational foundations of basic recursive function theory
- The genericity theorem and parametricity in the polymorphic \(\lambda\)- calculus
- Classical logic, storage operators and second-order lambda-calculus
- A general storage theorem for integers in call-by-name \(\lambda\)- calculus
- Algebraic proofs of cut elimination
- Adequacy for a lazy functional language with recursive and polymorphic types
- A domain-theoretic semantics of lax generic functions.
- Phase semantics for light linear logic
- Behavioural inverse limit -models
- Cut-elimination for a logic with definitions and induction
- From computation to foundations via functions and application: The \(\lambda\)-calculus and its webbed models
- Paths-based criteria and application to linear logic subsystems characterizing polynomial time
- Uniform Heyting arithmetic
- Typing and computational properties of lambda expressions
- Building continuous webbed models for system F
- Type-directed specialization of polymorphism.
- A sequent calculus for subtyping polymorphic types
- Dependent choice, `quote' and the clock
- A strong normalization result for classical logic
- On Takeuti's early view of the concept of set
- Combinatory logic with polymorphic types
- Graded modal dependent type theory
- Deverbal semantics and the Montagovian generative lexicon \(\Lambda \mathsf {Ty}_n\)
- Natural language inference in Coq
- Burali-Forti as a purely logical paradox
- Mechanized metatheory revisited
- Term-generic logic
- A note on subject reduction in (, )-Curry with respect to complete developments
- Cut-elimination for quantified conditional logic
- A relational account of call-by-value sequentiality
- A simple proof of second-order strong normalization with permutative conversions
- Inductive types and type constraints in the second-order lambda calculus
- On the convergence of reduction-based and model-based methods in proof theory
- Lambda-calcul, évaluation paresseuse et mise en mémoire
- A Type Theory for Probabilistic \lambda –calculus
- Failure of normalization in impredicative type theory with proof-irrelevant propositional equality
- On paths-based criteria for polynomial time complexity in proof-nets
- A Constructive Semantic Approach to Cut Elimination in Type Theories with Axioms
- Realizability algebras III: some examples
- Cogent: uniqueness types and certifying compilation
- On the versatility of open logical relations. Continuity, automatic differentiation, and a containment theorem
- Applications of type theory
- Higher-order unification with dependent function types
- Adding algebraic rewriting to the untyped lambda calculus (extended abstract)
- Programming and Proving with Classical Types
- Polymorphic higher-order termination
- A cubical language for Bishop sets
- An extension of system \(F\) with subtyping
- scientific article; zbMATH DE number 7577586 (Why is no real title available?)
- Prawitz, Proofs, and Meaning
- Program testing and the meaning explanations of intuitionistic type theory
- Free theorems and runtime type representations
- Strong normalization from an unusual point of view
- Linear logic
- Neo-Logicism and Its Logic
- Typed equivalence, type assignment, and type containment
- Operations on records
- Inductively defined types in the Calculus of Constructions
- Algebraic types in PER models
- Inductive-data-type systems
- A Survey of the Proof-Theoretic Foundations of Logic Programming
- Choice and independence of premise rules in intuitionistic set theory
- The existential fragment of second-order propositional intuitionistic logic is undecidable
- Reduction Free Normalisation for a proof irrelevant type of propositions
- Types, abstraction, and parametric polymorphism, part 2
- Formula normalizations in verification
- Theoretical computer science: computability, decidability and logic
- A direct computational interpretation of second-order arithmetic via update recursion
- Proving properties of typed \(\lambda\)-terms using realizability, covers, and sheaves
- Adjectival and adverbial modification: the view from modern type theories
- Mechanized subject expansion in uniform intersection types for perpetual reductions
- On a second-order version of Russellian theory of definite descriptions
- Toward a geometry for syntax
- Categorical proof-theoretic semantics
- Proof-theoretic methods in quantifier-free definability
- On the expressive power of schemes
- A note on logical PERs and reducibility. Logical relations strike again!
- Lambda galore
- A two-level linear dependent type theory
- Types, Tableaus and Gödel’s God in Isabelle/HOL
- Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
- A rationale for conditional equational programming
- On strong normalization and type inference in the intersection type discipline
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5625124)
