Module functions

Source

Expand description

Auto-generated module

🤖 Generated with SplitRS

Functions§

abstracting_gradual_typing_ty: AbstractingGradualTyping: AGT framework lifting predicates to gradual types
abstraction_nominal_ty: AbstractionNominal: ⟨a⟩t — nominal abstraction over fresh name a
abstraction_ty: Abstraction: λ.t (binder in de Bruijn — no variable name needed)
affine_type_ty: AffineType: a type that may be used at most once (weakening allowed)
affine_typing_ty: AffineTyping: affine typing judgment (weakening OK, no contraction)
algebraic_effect_type_ty: AlgebraicEffectType: a type for algebraic effects with operations Op
app
app2
app3
application_ty: Application: t s
applicative_order_redex_ty: ApplicativeOrderRedex: leftmost-innermost redex (call by value)
arrow
arrow_type_ty: ArrowType: function type A → B in simple type theory
bang_modality_ty: BangModality: the !A modality — unrestricted use of A
base_type_ty: BaseType: a ground/atomic type
beta_equiv_ty: BetaEquiv: β-equivalence (=β)
beta_redex_ty: BetaRedex: t is a beta redex iff t = (λ.s) u
beta_reduction_ty: BetaReduction: reflexive transitive closure of →β
beta_step: Perform one-step β-reduction under the given strategy.
beta_step_applicative
beta_step_head
beta_step_ty: BetaStep: one-step β-reduction t →β s
binary_session_typing_ty: BinarySessionTyping: Γ ⊢ P : S (binary session typing)
blame_calculus_term_ty: BlameCalculusTerm: a term in the blame calculus (with casts and labels)
blame_label_ty: BlameLabel: a label tracking the source of a runtime type failure
blame_theorem_ty: BlameTheorem: well-typed programs can only be blamed at boundaries
bohm_equiv_ty: BohmEquiv: two terms are Böhm-equal iff their Böhm trees are equal
bohm_theorem_ty: BohmTheorem: two distinct β-normal forms are separable by a context
bohm_tree_of_ty: BohmTreeOf: compute the Böhm tree of a term
bohm_tree_ty: BohmTree: the Böhm tree of a lambda term (possibly infinite)
bool_ty
bounded_quantification_ty: BoundedQuantification: ∀ X <: T. U (F-sub style bounded ∀)
build_lambda_calculus_env: Populate an Environment with lambda-calculus axioms and theorem stubs.
bvar
cbn_reduction_ty: CallByNeedReduction: lazy/sharing evaluation
cbv_reduction_ty: CallByValueReduction: strict/CBV evaluation
check_type: Type checking for the simply-typed lambda calculus. Returns true iff ctx ⊢ term : ty.
church: Build the Church numeral for n. c_n = λf. λx. f^n x
church_add: Apply PLUS to two Church numerals and reduce to normal form.
church_arith_correct_ty: ChurchArithCorrect: Church arithmetic is correct w.r.t. Nat arithmetic
church_bool_f_ty: ChurchEncoding_BoolF: System F encoding of booleans ∀ α. α → α → α
church_exp_ty: ChurchExp: exponentiation combinator E = λm.λn.n m
church_is_zero_ty: ChurchIsZero: test whether a Church numeral is zero
church_list_f_ty: ChurchEncoding_ListF: System F encoding of lists ∀ α β. β → (α → β → β) → β
church_mul: Church multiplication: MUL = λm. λn. λf. m (n f)
church_mul_ty: ChurchMul: multiplication combinator M = λm.λn.λf.m (n f)
church_nat_f_ty: ChurchEncoding_NatF: System F encoding of natural numbers ∀ α. (α → α) → α → α
church_numeral_correct_ty: ChurchNumeralCorrect: church_numeral n reduces to the standard encoding
church_numeral_ty: ChurchNumeral: the Church encoding of n as λf.λx.f^n x
church_plus: Church addition: PLUS = λm. λn. λf. λx. m f (n f x)
church_plus_ty: ChurchPlus: addition combinator M = λm.λn.λf.λx.m f (n f x)
church_pred_ty: ChurchPred: predecessor combinator (Kleene encoding)
church_rosser_theorem_ty: ChurchRosserTheorem: β-reduction is confluent
church_succ: Church successor: S = λn. λf. λx. f (n f x)
church_succ_ty: ChurchSucc: the successor combinator S = λn.λf.λx.f (n f x)
cic_elimination_ty: CICElimination: the elimination/recursor for an inductive type
cic_inductive_type_ty: CICInductiveType: an inductive type in the Calculus of Inductive Constructions
cic_positivity_condition_ty: CICPositivityCondition: strict positivity for inductive types
coc_sn_ty: CoCStrongNormalization: the Calculus of Constructions is SN
coc_ty: CoC: the Calculus of Constructions (top of the λ-cube)
coeffect_system_ty: CoeffectSystem: a type system tracking resource usage via graded types
coeffect_typing_ty: CoeffectTyping: Γ ⊢ t : T graded by r
coercion_function_ty: CoercionFunction: a coercion c : A → B witnessing A <: B
confluence_ty: Confluence: the reflexive transitive closure of →β has the diamond property
cst
cumulative_hierarchy_ty: CumulativeHierarchy: Uᵢ ⊆ Uᵢ₊₁ (lifting from one universe to the next)
deadlock_freedom_ty: DeadlockFreedom: well-typed session processes do not deadlock
delimited_continuation_ty: DelimitedContinuation: type of delimited continuation operators (shift/reset)
dependent_session_type_ty: DependentSessionType: a session type indexed by values (dependent sessions)
diamond_property_ty: DiamondProperty: if t →₁ u and t →₁ v then ∃ w, u →₁ w and v →₁ w
dual_session_ty: DualSession: the dual of a session type (swap sends and receives)
dyn_type_ty: DynType: the dynamic type ? (unknown type)
effect_label_ty: EffectLabel: a label for a computational effect
effect_set_ty: EffectSet: a set of effect labels
effect_type_ty: EffectType: a type annotated with effects τ !ε
effect_typing_ty: EffectTyping: Γ ⊢ t : τ ! ε
empty_row_ty: EmptyRow: the empty row
end_type_ty: EndType: the completed session
equi_recursive_type_ty: EquiRecursiveType: equi-recursive interpretation (fold/unfold invisible)
eta_redex_ty: EtaRedex: t is an eta redex iff t = λ.(s (BVar 0)) with BVar 0 not free in s
eta_step_ty: EtaStep: one-step η-reduction t →η s
extend_row_ty: ExtendRow: add a field l : T to a row R
f_bounded_polymorphism_ty: FBoundedPolymorphism: F-bounded quantification ∀ X <: F[X]. U
filter_model_ty: FilterModel: a filter model of the untyped λ-calculus via intersection types
flow_analysis_ty: FlowAnalysis: 0-CFA / control-flow analysis as a type system
freshness_predicate_ty: FreshnessPredicate: a # t — name a is fresh in term t
global_to_local_ty: GlobalToLocal: project a global type to a local session type for a role
graded_type_ty: GradedType: a type T graded by a semiring element r (coeffect)
gradual_type_ty: GradualType: a type that may be partially unknown (includes ?)
gradual_typing_ty: GradualTyping: Γ ⊢ t : A in the gradually-typed λ-calculus
handler_type_ty: HandlerType: a handler mapping effects to values of type A
head_normal_form_ty: HeadNormalForm: the head of t is not a redex
head_reduction_ty: HeadReduction: reduce the head redex (lazy evaluation)
higher_kinded_type_ty: HigherKindedType: a type constructor of kind κ ⇒ κ’
impl_pi
infer_type: Type inference for the simply-typed lambda calculus (Curry style). Returns Some(ty) if the term is typeable, None otherwise.
intersection_type_completeness_ty: IntersectionTypeCompleteness: every normalizable term is typeable
intersection_type_ty: IntersectionType: A ∩ B — a term has both types A and B
intersection_typing_ty: IntersectionTyping: Γ ⊢ t : A ∩ B
irrelevant_argument_ty: IrrelevantArgument: a term whose type-theoretic argument is proof-irrelevant
iso_recursive_fold_ty: IsoRecursiveFold: fold : F[μX.F] → μX.F
iso_recursive_unfold_ty: IsoRecursiveUnfold: unfold : μX.F → F[μX.F]
kind_arrow_ty: KindArrow: kind constructor A ⇒ B
kind_completeness_ty: KindCompleteness: kind inference is complete for Fω types
kind_inference_ty: KindInference: algorithm to infer kinds for type expressions
kind_polymorphism_ty: KindPolymorphism: ∀κ. F[κ] — quantification over kinds
kind_soundness_ty: KindSoundness: well-kinded type applications have well-kinded results
kind_ty: Kind: the kind language of System Fω (* and →)
lambda2_ty: Lambda2: System F corner of cube (type polymorphism)
lambda_arrow_ty: LambdaArrow: simply-typed lambda calculus corner of cube
lambda_omega_ty: LambdaOmega: System Fω corner (type constructors)
lambda_p_ty: LambdaP: λP (dependent types, Edinburgh LF)
lf_context_ty: LFContext: a context Γ in Edinburgh LF
lf_kind_validity_ty: LFKindValidity: Σ; Γ ⊢ K kind
lf_signature_ty: LFSignature: a signature Σ in Edinburgh LF
lf_typing_ty: LFTyping: Σ; Γ ⊢ t : T in Edinburgh LF
linear_arrow_ty: LinearArrow: the linear function type A ⊸ B
linear_context_ty: LinearContext: a linear typing context (each variable used exactly once)
linear_exchangeability_ty: LinearExchangeability: linear contexts can be reordered
linear_type_ty: LinearType: a type that must be used exactly once
linear_typing_ty: LinearTyping: linear typing judgment Γ ⊢_L t : A
liquid_type_ty: LiquidType: refinement type with decidable predicates (Liquid Haskell style)
list_ty
monadic_type_ty: MonadicType: a monadic type T M (T wrapped in monad M)
monadic_typing_ty: MonadicTyping: Γ ⊢ t : M[A] for monad M
multiparty_session_type_ty: MultipartySessionType: a global type for multiparty session protocols
nat_ty
nominal_type_ty: NominalType: a type with freshness/name-binding (nominal logic)
normal_form_ty: NormalForm: t has no β-redex
normal_order_redex_ty: NormalOrderRedex: leftmost-outermost redex
normal_order_strategy_ty: NormalOrderStrategy: normal order finds normal form if one exists
observational_equiv_ty: ObservationalEquiv: contextual equivalence in the untyped λ-calculus
occurrence_typing_ty: OccurrenceTyping: type assignment based on control flow occurrences
omega_combinator_ty: OmegaCombinator: Ω = (λx.x x)(λx.x x) — diverging term
omega_diverges_ty: OmegaDiverges: Ω has no normal form
option_ty
parallel_max_reduct_property_ty: ParallelMaxReductProperty: diamond property for complete development
parallel_max_reduct_ty: ParallelMaxReduct: complete parallel development
parallel_reduction_complete_ty: ParallelReductionComplete: t →β s implies t →β∥ s
parallel_reduction_ty: ParallelReduction: parallel β-reduction (β∥) — key for CR proof
pcf_adequacy_ty: PCFAdequacy: operational and denotational semantics agree for PCF
pcf_denotational_semantics_ty: PCFDenotationalSemantics: Scott domain semantics for PCF
pcf_fixpoint_ty: PCFFixpoint: the fixed-point operator fix : (τ → τ) → τ in PCF
pcf_full_abstraction_ty: PCFFullAbstraction: Milner’s full abstraction problem for PCF
pcf_term_ty: PCFTerm: terms of PCF (including fix, pred, succ, if-then-else)
pcf_type_ty: PCFType: types of PCF (Plotkin’s Programming Computable Functions) PCF = STLC + fixpoint + nat + bool
pcf_typing_ty: PCFTyping: typing judgment for PCF
pi
principal_typing_ty: PrincipalTyping: every typeable term has a principal type scheme
proof_irrelevance_ty: ProofIrrelevance: any two proofs of the same proposition are equal
prop
pts_axiom_ty: PTS_Axiom: the set of axioms (s : s’) for a pure type system
pts_confluence_ty: PTSConfluence: confluence holds for all PTS (β-reduction)
pts_rule_ty: PTS_Rule: the set of rules (s₁, s₂, s₃) for Π-type formation
pts_subject_reduction_ty: PTSSubjectReduction: subject reduction holds for all functional PTS
pts_typing_ty: PTSTyping: Γ ⊢ t : T in a PTS
pure_type_system_ty: PureTypeSystem: a PTS defined by sorts S, axioms A, rules R
quotient_computation_ty: QuotientComputation: [a] elim f = f a
quotient_elim_ty: QuotientElim: elimination from A / ~ to a P that respects ~
quotient_intro_ty: QuotientIntro: [a] : A / ~ (introduction rule)
quotient_type_ty: QuotientType: the quotient A / ~ of a setoid
record_type_ty: RecordType: a closed record type from a row
recursion_theorem_ty: RecursionTheorem: every function has a fixed point
recursive_type_contraction_ty: RecursiveTypeContraction: well-founded recursive types have unique fixed points
recursive_type_ty: RecursiveType: a type μX.F[X] — least fixed point of type functor F
recv_type_ty: RecvType: ?T.S — receive a value of type T then continue as S
refinement_type_ty: RefinementType: {x : T | P x} — a type refined by predicate P
region_inference_ty: RegionInference: algorithm to infer region annotations
region_type_ty: RegionType: a type annotated with memory region ρ
relevant_type_ty: RelevantType: a type that must be used at least once (contraction OK, no weakening)
relevant_typing_ty: RelevantTyping: relevant typing judgment
resizing_axiom_ty: ResizingAxiom: propositional resizing (all propositions are small)
row_polymorphic_typing_ty: RowPolymorphicTyping: Γ ⊢ t : {R} with row variable R
row_type_ty: RowType: a row of labeled types (for records or variants)
russell_universe_ty: RussellUniverse: Uᵢ : Uᵢ₊₁ in the Russell style (types live in universes)
send_type_ty: SendType: !T.S — send a value of type T then continue as S
session_type_completeness_ty: SessionTypeCompleteness: every interaction satisfying the global type is typeable
session_type_ty: SessionType: the type of a communication channel endpoint
setoid_carrier_ty: SetoidCarrier: the carrier set of a setoid
setoid_relation_ty: SetoidRelation: the equivalence relation of a setoid
setoid_ty: Setoid: a pair of a carrier and an equivalence relation
simple_type_ty: SimpleType: the type of simple types over a base type set
solvable_term_ty: SolvableTerm: a term with a head normal form
squash_elim_ty: SquashElim: ||A|| → (A → P) → P for P : Prop
squash_intro_ty: SquashIntro: a : A → ||A||
squash_type_ty: SquashType: propositional truncation ||A|| (collapse all proofs)
standardization_theorem_ty: StandardizationTheorem: if t has a normal form, normal order reaches it
star_kind_ty: StarKind: the base kind *
stlc_church_rosser_ty: STLCChurchRosser: STLC β-reduction is confluent
stlc_decidability_ty: STLCDecidability: type-checking STLC is decidable
stlc_strong_normalization_ty: STLCStrongNormalization: all well-typed STLC terms are strongly normalizing
stlc_subject_reduction_ty: STLCSubjectReduction: if Γ ⊢ t : τ and t →β s then Γ ⊢ s : τ
stlc_typing_ty: STLCTyping: Γ ⊢ t : τ (simple type assignment)
structural_subtyping_ty: StructuralSubtyping: subtyping determined by structure, not names
substitution_ty: Substitution: t[s/n] — substitute s for de Bruijn index n in t
subtype_relation_ty: SubtypeRelation: A <: B (A is a subtype of B)
subtyping_reflexivity_ty: SubtypingReflexivity: A <: A
subtyping_subject_reduction_ty: SubtypingSubjectReduction: subtying is preserved under reduction
subtyping_transitivity_ty: SubtypingTransitivity: A <: B → B <: C → A <: C
system_f_confluence_ty: SystemFConfluence: System F β-reduction is confluent
system_f_parametricity_ty: SystemFParametricity: Reynolds’s abstraction theorem
system_f_sn_ty: SystemFStrongNormalization: System F is strongly normalizing
system_f_term_ty: SystemFTerm: terms of System F (including type abstraction and application)
system_f_type_ty: SystemFType: types of System F (including type variables and ∀)
system_f_typing_ty: SystemFTyping: typing judgment for System F
system_f_undecidable_ty: SystemFUndecidableTyping: type inference for System F is undecidable (Wells)
system_fomega_kind_soundness_ty: SystemFOmegaKindSoundness: well-kinded types have sound interpretations
system_fomega_sn_ty: SystemFOmegaSN: Fω is strongly normalizing
system_fomega_term_ty: SystemFOmegaTerm: terms of System Fω
system_fomega_type_ty: SystemFOmegaType: types of System Fω
system_fomega_typing_ty: SystemFOmegaTyping: typing judgment for Fω
tarski_decode_ty: TarskiDecode: el : Uᵢ → Type (decode a code to a type)
tarski_universe_ty: TarskiUniverse: a Tarski-style universe Uᵢ with a decoding map elᵢ
turing_combinator_ty: TuringCombinator: Turing’s Θ fixed point combinator
type0
type1
type_consistency_ty: TypeConsistency: A ~ B (types are consistent, i.e., compatible under ?)
type_constructor_ty: TypeConstructor: a type-level function with a kind
type_unrolling_ty: TypeUnrolling: μX.F ≡ F[μX.F] (equi-recursive unrolling)
typing_context_ty: TypingContext: a finite map from variables to simple types
union_type_ty: UnionType: A ∪ B — occurrence typing context
universe_level_ty: UniverseLevel: the type of universe levels (ω-many levels)
universe_polymorphism_ty: UniversePolymorphism: quantification over universe levels
unsolvable_term_ty: UnsolvableTerm: a term with no head normal form
untyped_term_ty: UntypedTerm: the type of untyped lambda terms (de Bruijn representation)
utt_el_type_ty: UTTELType: a type in UTT (el-form, deriving a type from a set)
utt_universe_ty: UTTUniverse: a universe in Luo’s Unified Theory of Types
variable_ty: Variable: de Bruijn index n refers to the n-th enclosing binder
variant_type_ty: VariantType: a closed variant type from a row
weak_normal_form_ty: WeakNormalForm: t can be reduced to a normal form
y_combinator_ty: YCombinator: Curry’s Y = λf.(λx.f(x x))(λx.f(x x))
y_fixed_point_ty: YFixedPoint: Y f =β f (Y f)

Type Aliases§

UsageMap: Result of linearity checking: a map from de Bruijn level → usage count.

Module functions

Module functions Copy item path

Functions§

Type Aliases§

Module functions