scientific article
From MaRDI portal
Publication:3886868
zbMath0443.68039MaRDI QIDQ3886868
Publication date: 1979
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items
J-Calc: a typed lambda calculus for intuitionistic justification logic, Finitary higher inductive types in the groupoid model, Inductive families, Meaning and computing: two approaches to computable propositions, A Brief Overview of Agda – A Functional Language with Dependent Types, From operational semantics to abstract machines, Terminating general recursion, Lazy variable-renumbering makes substitution cheap, Algorithmic Theories of Problems. A Constructive and a Non-Constructive Approach, A set constructor for inductive sets in Martin-Löf's type theory, Meaning explanations at higher dimension, Canonicity and normalization for dependent type theory, C-system of a module over a \(Jf\)-relative monad, Level I theory of large deviations in the ideal gas, Unnamed Item, The significance of the ergodic decomposition of stationary measures for the interpretation of probability, The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories, Internal type theory, The Functional Interpretation of Direct Computations, Dependent Types at Work, Unnamed Item, Unnamed Item, Mollusc a general proof-development shell for sequent-based logics, On Ruelle's construction of the thermodynamic limit for the classical microcanonical entropy, The foundation of a generic theorem prover, Equivalences between pure type systems and systems of illative combinatory logic, Programs as proofs: A synopsis, Type Theory and Homotopy, Higher order functions and Brouwer’s thesis