scientific article; zbMATH DE number 3859117
From MaRDI portal
Publication:3328540
Recommendations
Cited in
(91)- A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction
- A small complete category
- On Church's formal theory of functions and functionals. The - calculus: Connections to higher type recursion theory, proof theory, category theory
- Between constructive mathematics and PROLOG
- Partial inductive definitions
- Static semantics, types, and binding time analysis
- Nonconstructive computational mathematics
- Predicative functionals and an interpretation of \({\widehat{\text{ID}}_{<\omega}}\)
- IMPS: An interactive mathematical proof system
- On the relationship between foundations of programming and mathematics
- Induction-recursion and initial algebras.
- Some points in formal topology.
- Proof-search in type-theoretic languages: An introduction
- The origins of structural operational semantics
- Middle-out reasoning for synthesis and induction
- A meaning explanation for HoTT
- Predicativity and constructive mathematics
- Formally computing with the non-computable
- A characterisation of elementary fibrations
- Towards a directed homotopy type theory
- A type-theoretic approach to program development
- The justification of identity elimination in Martin-Löf's type theory
- An adequacy theorem for dependent type theory
- From signatures to monads in \textsf{UniMath}
- Connectionist computations of intuitionistic reasoning
- Constructive algebraic integration theory
- A Classical Realizability Model for a Semantical Value Restriction
- Homotopy type theory and Voevodsky's univalent foundations
- Turing-Completeness Totally Free
- Intuitionistic ancestral logic as a dependently typed abstract programming language
- A proposal for broad spectrum proof certificates
- From mathesis universalis to provability, computability, and constructivity
- RZ: a Tool for Bringing Constructive and Computable Mathematics Closer to Programming Practice
- Building Mathematics-Based Software Systems to Advance Science and Create Knowledge
- scientific article; zbMATH DE number 3936476 (Why is no real title available?)
- scientific article; zbMATH DE number 4006266 (Why is no real title available?)
- Intuitionistic completeness of first-order logic
- scientific article; zbMATH DE number 53194 (Why is no real title available?)
- scientific article; zbMATH DE number 130887 (Why is no real title available?)
- Constructive Mathematics in Theory and Programming Practice
- Reading between the lines in constructive type theory
- Using formal methods with SysML in aerospace design and engineering
- An introduction to univalent foundations for mathematicians
- The concept \textit{horse} is a concept
- Categories with families: unityped, simply typed, and dependently typed
- A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
- Internal parametricity for cubical type theory
- Applications of type theory
- Cubical methods in homotopy type theory and univalent foundations
- Type theory as a foundation for computer science
- Some normalization properties of Martin-Löf's type theory, and applications
- A generic algebra for data collections based on constructive logic
- POPLMark reloaded: mechanizing proofs by logical relations
- W-types in setoids
- scientific article; zbMATH DE number 3894466 (Why is no real title available?)
- Exploring abstract algebra in constructive type theory
- Eta-rules in Martin-Löf type theory
- Natural Deduction for Equality: The Missing Entity
- Truth and proof in intuitionism
- Program testing and the meaning explanations of intuitionistic type theory
- Constructivity in computer science. Summer symposium, San Antonio, TX, June 19--22, 1991. Proceedings
- Constructive Mathematics and Functional Programming (Abstract)
- A First Look into a Formal and Constructive Approach for Discrete Geometry Using Nonstandard Analysis
- Theory of Constructive Semigroups with Apartness – Foundations, Development and Practice
- The practice of logical frameworks
- From type theory to setoids and back
- A higher-order interpretation of deductive tableau
- On the proof theory of Coquand's calculus of constructions
- Finitary type theories with and without contexts
- A Survey of the Proof-Theoretic Foundations of Logic Programming
- Univalent Foundations and the UniMath Library
- A Comparison of Type Theory with Set Theory
- Process calculus based upon evaluation to committed form
- Martin-Löf identity types in C-systems
- Coalgebras in functional programming and type theory
- Programming by example and proving by example using higher-order unification
- A comparison of HOL and ALF formalizations of a categorical coherence theorem
- Importing mathematics from HOL into Nuprl
- Topological quantum gates in homotopy type theory
- The quantum monadology
- Comodule representations of second-order functionals
- The category of iterative sets in homotopy type theory and univalent foundations
- Handling mobility failures by modal types
- On different ways of being equal
- Paradoxical connectives: proof-theoretic semantics, recursion, and fixed-point operators
- Strict universes for Grothendieck topoi
- Nothing new under the sum: a formal model of fast Fourier algorithms
- Applause: An implementation of the Collins-Michalski theory of plausible reasoning
- Insight in discrete geometry and computational content of a discrete model of the continuum
- Constructive system for automatic program synthesis
- A computer-verified monadic functional implementation of the integral
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 Q3328540)
