The following pages link to Automath (Q19182):
Displaying 50 items.
- The HOL Light theory of Euclidean space (Q1945903) (← links)
- Relational hidden variables and non-locality (Q1956376) (← links)
- Towards a formal framework for heterogeneous relation algebra (Q1961865) (← links)
- A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L (Q1961914) (← links)
- Some lambda calculus and type theory formalized (Q1961921) (← links)
- Term-space semantics of typed lambda calculus (Q1981989) (← links)
- Automated deduction and knowledge management in geometry (Q1995808) (← links)
- The universal exponentiable arrow (Q2078410) (← links)
- Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL (Q2102946) (← links)
- On preserving the computational content of mathematical proofs: toy examples for a formalising strategy (Q2117791) (← links)
- \texttt{slepice}: towards a verified implementation of type theory in type theory (Q2119108) (← links)
- Combinatory logic with polymorphic types (Q2144609) (← links)
- Analysis in a formal predicative set theory (Q2148788) (← links)
- Exploring the structure of an algebra text with locales (Q2209550) (← links)
- Substitution contradiction, its resolution and the Church-Rosser theorem in TIL (Q2301323) (← links)
- A note on algebraic semantics for \(\mathsf {S5}\) with propositional quantifiers (Q2319895) (← links)
- An analytic calculus for the intuitionistic logic of proofs (Q2330501) (← links)
- Taxonomies of geometric problems (Q2334578) (← links)
- Towards semantic mathematical editing (Q2348287) (← links)
- Mechanizing metatheory without typing contexts (Q2352491) (← links)
- A short note on type-inhabitation: formula-trees vs. game semantics (Q2353633) (← links)
- Quantum computation with programmable connections between gates (Q2376283) (← links)
- Type theory and formalisation of mathematics (Q2399357) (← links)
- A survey of strategies in rule-based program transformation systems (Q2456575) (← links)
- Information and knowledge. A constructive type-theoretical approach (Q2464131) (← links)
- A proof-theoretic foundation of abortive continuations (Q2464725) (← links)
- On the mechanization of the proof of Hessenberg's theorem in coherent logic (Q2471743) (← links)
- Classical \(F_{\omega}\), orthogonality and symmetric candidates (Q2482840) (← links)
- Investigations on the dual calculus (Q2503329) (← links)
- A modern elaboration of the ramified theory of types (Q2563450) (← links)
- Equivalences between pure type systems and systems of illative combinatory logic (Q2565990) (← links)
- A simple proof of second-order strong normalization with permutative conversions (Q2566069) (← links)
- Genericity and the \(\pi\)-calculus (Q2576663) (← links)
- From realizability to induction via dependent intersection (Q2636522) (← links)
- A higher-order calculus and theory abstraction (Q2639838) (← links)
- Procedural representation of CIC proof terms (Q2655331) (← links)
- Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge (Q2663667) (← links)
- CINNI -- a generic calculus of explicit substitutions and its application to \(\lambda\)-, \(\sigma\)- and \(\pi\)-calculi (Q2703692) (← links)
- Pure type systems with explicit substitution (Q2713351) (← links)
- Perpetuality in a named lambda calculus with explicit substitutions (Q2713353) (← links)
- Dependent types and explicit substitutions: A meta-theoretical development (Q2713354) (← links)
- Domain-free \(\lambda\mu\)-calculus (Q2729625) (← links)
- Coalgebras for binary methods: Properties of bisimulations and invariants (Q2747943) (← links)
- (Q2754030) (← links)
- (Q2754063) (← links)
- (Q2763649) (← links)
- A formal framework for managing mathematics (Q2767940) (← links)
- (Q2778821) (← links)
- Scalar System F for linear-algebraic \(\lambda\)-calculus: towards a quantum physical logic (Q2825375) (← links)
- Strong normalization with singleton types (Q2842835) (← links)
