The following pages link to (Q3994895):
Displaying 50 items.
- Structuring co-constructive logic for proofs and refutations (Q263109) (← links)
- On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem (Q265002) (← links)
- J-Calc: a typed lambda calculus for intuitionistic justification logic (Q276037) (← links)
- Computation by interaction for space-bounded functional programming (Q276265) (← links)
- Category theory, logic and formal linguistics: some connections, old and new (Q280832) (← links)
- Atomicity, coherence of information, and point-free structures (Q290637) (← links)
- A decidable theory of type assignment (Q365669) (← links)
- Intuitionistic completeness of first-order logic (Q392280) (← links)
- Classical logic with partial functions (Q438568) (← links)
- Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control (Q444460) (← links)
- A constructive analysis of learning in Peano arithmetic (Q450942) (← links)
- The complexity of higher-order queries (Q498405) (← links)
- Prior's tonk, notions of logic, and levels of inconsistency: vindicating the pluralistic unity of science in the light of categorical logical positivism (Q516400) (← links)
- Computing the Lagrangians of the standard model II. The ghost term (Q517688) (← links)
- The vectorial \(\lambda\)-calculus (Q529049) (← links)
- Yet another bijection between sequent calculus and natural deduction (Q530853) (← links)
- Preface to the special volume (Q534064) (← links)
- Musings around the geometry of interaction, and coherence (Q534708) (← links)
- Realizability models and implicit complexity (Q534712) (← links)
- Polarized and focalized linear and classical proofs (Q556824) (← links)
- Cut-elimination in the strict intersection type assignment system is strongly normalizing (Q558418) (← links)
- Strong normalisation in the \(\pi\)-calculus (Q598201) (← links)
- Nominal abstraction (Q617715) (← links)
- Set systems: order types, continuous nondeterministic deformations, and quasi-orders (Q653312) (← links)
- Linearity and iterator types for Gödel's system \(\mathcal T\) (Q656851) (← links)
- Intersection type assignment systems with higher-order algebraic rewriting (Q672048) (← links)
- Towards a proof theory of rewriting: The simply typed \(2\lambda\)-calculus (Q672060) (← links)
- On maximal stable functions (Q673145) (← links)
- Genetic programming \(+\) proof search \(=\) automatic improvement (Q682376) (← links)
- Comparing Hagino's categorical programming language and typed lambda- calculi (Q685425) (← links)
- Computational interpretations of linear logic (Q685430) (← links)
- Representation and duality of the untyped \(\lambda\)-calculus in nominal lattice and topological semantics, with a proof of topological completeness (Q730088) (← links)
- Pedagogical second-order \(\lambda \)-calculus (Q732007) (← links)
- Intuitionistic hybrid logic: introduction and survey (Q764256) (← links)
- Strong normalization of \(\mathsf{ML}^{\mathsf F}\) via a calculus of coercions (Q764331) (← links)
- Systems of combinatory logic related to Quine's `New Foundations' (Q809994) (← links)
- Towards a semantic characterization of cut-elimination (Q817704) (← links)
- A semantical proof of the strong normalization theorem for full propositional classical natural deduction (Q818927) (← links)
- Coq formalization of the higher-order recursive path ordering (Q843949) (← links)
- Directly reflective meta-programming (Q848742) (← links)
- Simplifying proofs in Fitch-style natural deduction systems (Q851139) (← links)
- An effective proof of the well-foundedness of the multiset path ordering (Q857884) (← links)
- A (restricted) quantifier elimination for security protocols (Q860909) (← links)
- Innovations in computational type theory using Nuprl (Q865639) (← links)
- The Girard-Reynolds isomorphism (second edition) (Q879366) (← links)
- The faithfulness of \(\mathbf{F_{at}}\): a proof-theoretic proof (Q897484) (← links)
- Nominal techniques in Isabelle/HOL (Q928672) (← links)
- On strong normalization and type inference in the intersection type discipline (Q930868) (← links)
- The heart of intersection type assignment: Normalisation proofs revisited (Q930869) (← links)
- A typed lambda calculus with intersection types (Q930870) (← links)
