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