The following pages link to (Q5638283):
Displaying 46 items.
- An intuitionistic version of Ramsey's theorem and its use in program termination (Q499082) (← links)
- Equational theories for inductive types (Q678762) (← links)
- Another proof of the intuitionistic Ramsey theorem (Q685402) (← links)
- Partial inductive definitions as type-systems for \(\lambda\)-terms (Q688729) (← links)
- On systems of definitions, induction and recursion (Q688731) (← links)
- Type-theoretic interpretation of iterated, strictly positive inductive definitions (Q688845) (← links)
- Partial inductive definitions (Q1177153) (← links)
- An intuitionistic theory of types with assumptions of high-arity variables (Q1192333) (← links)
- Theory of proofs (arithmetic and analysis) (Q1260035) (← links)
- Inductive families (Q1336951) (← links)
- Representing inductively defined sets by wellorderings in Martin-Löf's type theory (Q1392287) (← links)
- Cut-elimination for a logic with definitions and induction (Q1575931) (← links)
- Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs (Q1798782) (← links)
- Cut elimination for a logic with induction and co-induction (Q1948276) (← links)
- Non-well-founded deduction for induction and coinduction (Q2055840) (← links)
- Integrating induction and coinduction via closure operators and proof cycles (Q2096458) (← links)
- The harmony of identity (Q2281316) (← links)
- The justification of identity elimination in Martin-Löf's type theory (Q2288279) (← links)
- Proof, meaning and paradox: some remarks (Q2288280) (← links)
- On the unity of duality (Q2482843) (← links)
- Failure of completeness in proof-theoretic semantics (Q2516584) (← links)
- Logicality, double-line rules, and modalities (Q2631645) (← links)
- Proof-theoretic harmony: towards an intensional account (Q2695033) (← links)
- Inductive Completeness of Logics of Programs (Q2804944) (← links)
- Well-Partial Orderings and their Maximal Order Types (Q3295157) (← links)
- Restricting Initial Sequents: The Trade-Offs Between Identity, Contraction and Cut (Q3305560) (← links)
- From Mathesis Universalis to Provability, Computability, and Constructivity (Q3305633) (← links)
- Dialogues, Reasons and Endorsement (Q3305643) (← links)
- Cut-Elimination and Proof Schemata (Q3455184) (← links)
- On the Completeness of Dynamic Logic (Q3617722) (← links)
- Lexicographic Path Induction (Q3637202) (← links)
- Some derived rules of intuitionistic second order arithmetic (Q4159055) (← links)
- Algorithmic Theories of Problems. A Constructive and a Non-Constructive Approach (Q4565827) (← links)
- An introduction to univalent foundations for mathematicians (Q4684362) (← links)
- Can You Add Power‐Sets to Martin‐Lof's Intuitionistic Set Theory? (Q4704657) (← links)
- Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent (Q5079741) (← links)
- Dependent Types at Work (Q5191088) (← links)
- Prawitz, Proofs, and Meaning (Q5213604) (← links)
- Explaining Deductive Inference (Q5213606) (← links)
- Iterated Inductive Definitions Revisited (Q5214787) (← links)
- (Q5227521) (← links)
- An Approach to General Proof Theory and a Conjecture of a Kind of Completeness of Intuitionistic Logic Revisited (Q5251195) (← links)
- A new connective in natural deduction, and its application to quantum computing (Q5925711) (← links)
- Least and greatest fixed points in intuitionistic natural deduction (Q5958300) (← links)
- SUBATOMIC INFERENCES: AN INFERENTIALIST SEMANTICS FOR ATOMICS, PREDICATES, AND NAMES (Q6051421) (← links)
- A Survey of the Proof-Theoretic Foundations of Logic Programming (Q6063891) (← links)
