The duality of computation
From MaRDI portal
Recommendations
Cited in
(only showing first 100 items - show all)- Focusing and polarization in linear, intuitionistic, and classical logics
- Classical realizability in the CPS target language
- Classical natural deduction for S4 modal logic
- Polarized games
- Parametric parameter passing \(\lambda\)-calculus
- Proof nets for classical logic
- Abstracting models of strong normalization for classical calculi
- Quantitative classical realizability
- Classical \(F_{\omega}\), orthogonality and symmetric candidates
- Strong normalization of classical natural deduction with disjunctions
- Call-by-name reduction and cut-elimination in classical logic
- On the unity of duality
- Investigations on the dual calculus
- Declarative representation of proof terms
- Control categories and duality: On the categorical semantics of the lambda-mu calculus
- Call-By-Push-Value from a Linear Logic Point of View
- Classical by-need
- Compositional semantics for composable continuations: from abortive to delimited control
- Adjunction models for call-by-push-value with stacks
- Computing (and Life) Is All about Tradeoffs
- On the computational representation of classical logical connectives
- Reduction and conversion strategies for the calculus of (co)inductive constructions. I
- Probabilistic operational semantics for the lambda calculus
- The lambda -bar calculus, a dual calculus for unconstrained strategies
- Proofs, tests and continuation passing style
- Dualized simple type theory
- A classical sequent calculus with dependent types
- Classical call-by-need and duality
- A Filter Model for the λμ-Calculus
- Covert movement in logical grammar
- Intersection types for the resource control lambda calculi
- A formal language for cyclic operads
- The duality of computation under focus
- Open call-by-value
- Linear is CP (more or less)
- Classical proofs as parallel programs
- Call-by-Name and Call-by-Value in Normal Modal Logic
- Call-by-Value Is Dual to Call-by-Name, Extended
- Control reduction theories: the benefit of structural substitution
- The Logic of Proofs as a Foundation for Certifying Mobile Computation
- Dual Calculus with Inductive and Coinductive Types
- An Operational Account of Call-by-Value Minimal and Classical λ-Calculus in “Natural Deduction” Form
- On the Values of Reducibility Candidates
- A Logically Saturated Extension of ${{\bar\lambda\mu\tilde{\mu}}}$
- Monadic Translation of Intuitionistic Sequent Calculus
- Focalisation and Classical Realisability
- scientific article; zbMATH DE number 4088936 (Why is no real title available?)
- Semantic types and approximation for Featherweight Java
- Justification logic as a foundation for certifying mobile computation
- Böhm theorem and Böhm trees for the \(\varLambda \mu\)-calculus
- scientific article; zbMATH DE number 1948183 (Why is no real title available?)
- Proving termination of evaluation for system F with control operators
- The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: a proof via corresponding calculus
- Game semantics and the geometry of backtracking: a new complexity analysis of interaction
- A note on strong normalization in classical natural deduction
- Beyond polarity: towards a multi-discipline intermediate language with sharing
- A Fresh Look at the λ-Calculus
- scientific article; zbMATH DE number 7204443 (Why is no real title available?)
- Compiling with classical connectives
- An extended type system with lambda-typed lambda-expressions
- The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem
- Models of Linear Logic based on the Schwartz \varepsilon-product
- Non-idempotent types for classical calculi in natural deduction style
- Deriving natural deduction rules from truth tables
- Expansion trees with cut
- Curry-Howard for sequent calculus at last!
- Classical Logic with Mendler Induction
- Classical realizability and arithmetical formulæ
- Call-by-name extensionality and confluence
- Strong Normalisation of Cut-Elimination That Simulates β-Reduction
- Term Rewriting and Applications
- Normalization in the simply typed -calculus
- Focused linear logic and the \(\lambda\)-calculus
- Proof Terms for Generalized Natural Deduction
- scientific article; zbMATH DE number 7713500 (Why is no real title available?)
- Classical (co)recursion: Mechanics
- Stateful Realizers for Nonstandard Analysis
- Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic
- Galois connecting call-by-value and call-by-name
- A framework for substructural type systems
- Kripke models for classical logic
- Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\)
- A strong bisimulation for a classical term calculus
- Theoretical computer science: computability, decidability and logic
- Strong call-by-value and multi types
- Focusing Gentzen's LK proof system
- Exponentials as substitutions and the cost of cut elimination in linear logic
- Positive focusing is directly useful
- Semi-axiomatic sequent calculus
- Permutability in proof terms for intuitionistic sequent calculus with cuts
- Bounded inquisitive logics: sequent calculi and schematic validity
- Mirroring call-by-need, or values acting silly
- Meaningfulness and genericity in a subsuming framework (invited talk)
- Proof search in classical propositional logic with partial proof terms
- On the cut-elimination of the modal -calculus: linear logic to the rescue
- Herbrand schemes for cyclic proofs
- A contextual formalization of structural coinduction
- Dual counterpart intuitionistic logic
- Equivalence of eval-readback and eval-apply big-step evaluators by structuring the lambda-calculus's strategy space
- Mirroring call-by-need, or values acting silly
This page was built for publication: The duality of computation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2943375)
