scientific article; zbMATH DE number 3692654

Cited in

(32)

On Ruelle's construction of the thermodynamic limit for the classical microcanonical entropy
Programs as proofs: A synopsis
Terminating general recursion
Lazy variable-renumbering makes substitution cheap
The significance of the ergodic decomposition of stationary measures for the interpretation of probability
Inductive families
Meaning explanations at higher dimension
The foundation of a generic theorem prover
Finitary higher inductive types in the groupoid model
Meaning and computing: two approaches to computable propositions
Canonicity and normalization for dependent type theory
Equivalences between pure type systems and systems of illative combinatory logic
C-system of a module over a \(Jf\)-relative monad
J-Calc: a typed lambda calculus for intuitionistic justification logic
The biequivalence of locally Cartesian closed categories and Martin-Löf type theories
A Brief Overview of Agda – A Functional Language with Dependent Types
From operational semantics to abstract machines
Algorithmic theories of problems. A constructive and a non-constructive approach
Internal type theory
Higher order functions and Brouwer's thesis
Cubical syntax for reflection-free extensional equality
Quotients, inductive types, and quotient inductive types
A set constructor for inductive sets in Martin-Löf's type theory
The functional interpretation of direct computations
Dependent Types at Work
\textit{Mollusc}: a general proof-development shell for sequent-based logics
Type theory and homotopy
PML2: integrated program verification in ML
Analyticity and syntheticity in type theory revisited
Frege on knowing the fundamental laws of logic
The equivariant model structure on cartesian cubical sets
Level I theory of large deviations in the ideal gas

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3886868)