scientific article; zbMATH DE number 7243672
From MaRDI portal
Publication:5119390
Publication date: 4 September 2020
Full work available at URL: https://arxiv.org/abs/1602.04860
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items (3)
A dual-context sequent calculus for the constructive modal logic S4 ⋮ UNDER LOCK AND KEY: A PROOF SYSTEM FOR A MULTIMODAL LOGIC ⋮ Unnamed Item
Uses Software
Cites Work
- Does the deduction theorem fail for modal logic?
- On the unity of logic
- Constructive modal logics. I
- Notions of computation and monads
- Combinatory logic. With two sections by William Craig.
- The modal logic of provability: cut-elimination
- Lectures on the Curry-Howard isomorphism
- The modal logic of provability. The sequential approach
- A modal sequent calculus for a fragment of arithmetic
- Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi
- LCF considered as a programming language
- On the strong normalisation of intuitionistic natural deduction with permutation-conversions
- Linear logic and elementary time
- On an intuitionistic modal logic
- Fitch-style modal lambda calculi
- Circular proofs for the Gödel-Löb provability logic
- A judgmental reconstruction of modal logic
- A theory of effects and resources: adjunction models and polarised calculi
- VALENTINI’S CUT-ELIMINATION FOR PROVABILITY LOGIC RESOLVED
- Computational Semantics with Functional Programming, by Jan van Eijck and Christina Unger .
- The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
- Introduction to Categories and Categorical Logic
- First steps in synthetic guarded domain theory: step-indexing in the topos of trees
- A Temporal Logic Approach to Binding-Time Analysis
- A modal analysis of staged computation
- A Terminating and Confluent Linear Lambda Calculus
- Proving Noninterference by a Fully Complete Translation to the Simply Typed lambda-calculus
- A natural extension of natural deduction
- Church-Rosser theorem for typed functional systems
- On the proof theory of the modal logic for arithmetic provability
- Logic Programming with Focusing Proofs in Linear Logic
- Computational types from a logical perspective
- Categories for Types
- Guard Your Daggers and Traces: Properties of Guarded (Co-)recursion
- Brouwer's fixed-point theorem in real-cohesive homotopy type theory
- Symbolic Representations of the Post-apartheid University
- Propositions as [Types]
- Quantum Gauge Field Theory in Cohesive Homotopy Type Theory
- A Generalized Modality for Recursion
- Degrees of Relatedness
- Pure type systems with corecursion on streams
- A semantic model for graphical user interfaces
- Modalities in homotopy type theory
- Productive coprogramming with guarded recursion
- Higher-order functional reactive programming without spacetime leaks
- Constructive Modalities with Provability Smack
- Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes
- Deciding equivalence with sums and the empty type
- Semantical Analysis of Modal Logic I Normal Modal Propositional Calculi
- The elimination theorem when modality is present
- A Logical Foundation for Environment Classifiers
- Parallel reductions in \(\lambda\)-calculus
- Primitive recursion for higher-order abstract syntax
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication:
