Flashcards

..According to computability theory, why do we split type checkers from parsers?According to robert (bob) harper, what are symbol, symbolic parameter and indexed operator?According to robert (bob) harper, what is a sort, syntactically?According to robert (bob) harper, what is a variable?According to robert (bob) harper, what is an operator, the arity of an operator?According to robert (bob) harper, what is the scope of a binding?According to robert (bob) harper, what is (type) safety?An evaluation statement is derivable iff there exists which derivation tree?Are languages inherently compiled/interpreted?Are normal forms always a value?Are runtime type errors a per-language choice?Are there booleans, strings, numbers defined in rocq?Are there many built-in features in rocq?Are values always in normal form?Between if-splitting and conditionals, which one can introduce unions, which one eliminates?Can a language implementer choose whether to compile or interpret a given language?Can a term fall within multiple syntactic categories?Can recursion be obtained through desugaring alone in symply typed lambda calculus?Can safe statically typed languages do away with dynamic checks?Can the type system totally not require interaction with or guidance from the programmers?Define boolean operations and, or, not for church booleans?Define successor, addition, multiplication, zero test, subtraction, predecessor, equality for church numerals?Disadvantages and advantages of union types compared to sum types?Does a language specify how it should be evaluated?Does a REPL enforce a kind of implementation (compilation/interpretation)?Does rust allow linking of different versions of a crate to the same binary, and how?Does the choice of evaluation strategy significantly affect the type system?Does unsafe language provide any static type checking at all?Flashcard Formalize function application and describe its notation in pure lambda calculus?Formalize the notion of being closed under renaming and substitution for variables and closed under renaming for symbolic parameters, in the context of uniformity of a rule?Functions that diverge vs functions that can fail?Given an equivalence relation r, what does "up to r" mean?How are derivations visualized?How are the hypotheses named if there are multiple in rocq?How are types and tests complementary?How can a set of evaluation rules enforce an evaluation strategy?How can the inductive definition define terms as trees?How do we make sure the formal derivability judgment behaves as an expected derivability judgment How do we make sure the formal generic judgment behaves as an expected generic judgment How does derivability differ from admissibility?How does generic judgment differ from parametric judgment?How does the "flow typing" concept relate to the "parse, do not validate" principle and "boolean blindness"?How does the "parse, do not validate" principle relate to "boolean blindness"?How does the principle of rule induction apply to the case simultaneous inductive definitions?How has computer science contributed to logic?How is a type checker different from a proof checker?How is generic derivability judgment defined?How is language safety different from static type safety How is parametric derivability judgment defined?How is the type "bool -> bool" pronounced in rocq?How must the concept of uniformity of a rule be extended?How to allow methods to reference each other using lexical scoping?How to allow private members to access public members using lexical scoping?How to define a days-of-week data type in rocq?How to define a tuple type in rocq?How to define an enumerated type in rocq?How to define an infix notation with a predefined fixity and precedence in rocq?How to define multi-argument functions in rocq?How to define recursive functions in rocq?How to define recursive types in rocq?How to destruct multiple variables at once in rocq?How to desugar letrec in racket?How to encode booleans and conditionals using church booleans in lambda calculus?How to encode multiple arguments in lambda calculus?How to encode pairs in lambda calculus?How to get the type of an expression in rocq?How to implement classes with prototypes?How to implement inheritance using lexical scoping?How to implement open recursion with self-application?How to implement self-reference with and without mutation?How to introduce infix syntax in rocq?How to invoke a function in rocq?How to make accessors on sum types safe?How to merge multiple patterns in a match arm in rocq?How to pattern match multiple expressions at once?How to place declarations inside a module in rocq?How to specify a theorem with a hypothesis in rocq?How to use fix to define recursive functions?How to use inductive definition to define functions?How to use the simpl tactic with a hypothesis?How to utilize the property of word-aligned addresses to optimize number How to verify the type of an expression in rocq?How to write a derivability judgment and what does it mean?How to write an admissibility judgment and what does it mean?In a generic rule, what are global variables and local variables?In a hypothetical rule, what does deriving a premise involve?In a pre-2018 survey, which two features were the most confusing?In an ABT, what is the valence of an argument?In an unsafe language, how can the system be disrupted?In computability theory terms, what are the differences between parsers and type checkers?In how many stages does the transformation from concrete syntax to abstract syntax undergo?In pure lambda calculus, what are the built-in constants and primitive operators?In rocq, what does types and values have to do with theorems and proofs?In rocq, which values can block simplification?In which application is strong normalization desirable?In which evaluation strategy, the one-step evaluation relation is a partial function on terms?In which style do the inductive definition and the inference rule format describe the syntax of a language?In which ways the lambda calculus can be viewed?Is a rust crate aware of its name?Is bullet point optional in subgoals in a destruct tactic? if yes, why would you use it?Is function signature compulsory in rocq?Is inheritance = subtyping?Is language safety absolute?Language safety from the perspective of trapped and untrapped errors?List some reasons why the rust crates ecosystem is robust?Name some classical heavyweight formal methods Name some lightweight formal methods Other than hypotheses, what can be used with rewrite tactics in rocq?Should we think in features or paradigms regarding programming languages?Showing that derivability is strictly stronger than admissibility The definition of runtime type error The definition of type system The relation between an evaluator and an interpreter?The relation between the set of values and the set of terms?To understand how a program may misbehave in an unsafe language, what should the programmer do?To which degree can type systems catch bad behaviors?Trait vs mixin?Using robert (bob) harper What are closed terms, free variables, bound variables, binders in lambda calculus?What are combinators in lambda calculus?What are computation and congruence rules?What are constructor expressions in rocq?What are induction hypothesis and induction conclusion?What are iterated and simultaneous inductive definition?What are judgment/assertion, judgment form, judgment instance, judgment form instance What are lambda terms and lambda abstractions?What are language concepts precisely described by?What are local hypothesis vs global hypothesis?What are nominal typing and structural typing?What are simpl, reflexivity in rocq?What are some challenges of retrofitting type systems?What are some examples of automated theorem provers?What are some problems with static types that make avoiding runtime errors impossible?What are some representations for natural numbers? what did we choose in rocq?What are some senses of the word "functional" in "functional programming"?What are some structural properties of admissibility?What are some ways to define the syntax of a language?What are substitution target and subject?What are the 2 definitions of substitution used in TAPL? for what purposes?What are the approaches to implementing macros?What are the approaches to typing conditionals and their tradeoffs?What are the benefits of functional programming?What are the cons of classical heavyweight formal methods What are the cons of lightweight formal methods What are the desirable properties of the evaluation relation there can be in a system?What are the differences between abstract and concrete syntax?What are the differences between rust crates and rust modules?What are the differences between terms and expressions?What are the general strategies for handling partiality in type systems?What are the ideal use cases of ASTs?What are the ideas of forward chaining and backward chaining?What are the ideas of forward chaining search and backward chaining search?What are the ideas of micro and macro gradual typings?What are the key considerations in designing conditionals?What are the major advantages of denotational semantics?What are the methods of finding derivations?What are the possible evaluation strategies for lambda calculus?What are the pros and cons of automated theorem provers?What are the pros and cons of backward chaining search?What are the pros and cons of forward chaining search?What are the pros and cons of proof assistants?What are the pros of classical heavyweight formal methods What are the pros of lightweight formal methods What are the structural properties of generic derivability judgment, governing the behavior of variables, if the rules are uniform?What are the syntax/values/evaluation relation for the untyped lambda calculus?What are the two broad categories of software tools for helping constructs proofs of logical propositions?What are the two forms of general judgments?What are the use cases of rocq?What are the uses for the first type system in fortran?What are the uses of the self-application pattern?What are theorem, lemma, fact, remark in rocq?What are there in the rocq system besides the kernel?What are two notions of entailment?What are type systems good for?What can a hypothetical inductive definition be ragarded as an ordinary inductive definition of?What can an evidence for admissibility be thought of as?What can functional programming refer to?What can static and dynamic semantics do?What do general judgments codify?What do generic judgments codify?What do hypothetical judgments codify?What do parametric judgments codify?What do programming languages describe, and for whom?What does a set of hypothetical rules $mathcal{r}$ define?What does abstract syntax have to do with AST/labeled tree?What does an inductive definition in rocq do?What does it mean by "everything is a function" in lambda calculus?What does it mean by the judgment $gamma dash_mathcal{r} k$, where $gamma$ is a finite set of basic judgments, $k$ is a basic judgment and $mathcal{r}$ is a set of rules?What does it mean by the judgment $dash_mathcal{r} gamma$, where $gamma$ is a finite set of basic judgments and $mathcal{r}$ is a set of rules?What does it mean by the judgment $dash_mathcal{r} k$, where $k$ is a basic judgment and $mathcal{r}$ is a set of rules?What does it mean for a collection of inference rules to form the strongest judgment form that is closed under those rules?What does it mean to say church numerals represent ordinary numbers?What does lambda calculus consist of in its purest form?What does structurality mean?What does the abort command do in rocq?What does the admitted command do in rocq?What does the evidence for generic derivability consist of?What does the intros tactic do?What does the principle of complete induction state?What does the principle of lexicographic induction state?What does the principle of ordinary induction state?What does the principle of rule induction state?What does the transition function do in the structural operational semantics?What does uniformity enable? what does it have to the implicit/local form?What does "variables in an AST range over some specified sorts" mean?What else can a type system catch other than low-level faults such as invoking non-existent methods What if some hypotheses are not derivable relative to $mathcal{r}$, then what do we deem the corresponding admissibility judgment as?What is a binding?What is a block in programming language?What is a closure in programming language?What is a common pattern of many reactive systems?What is a congruence?What is a countable set?What is a derived form in lambda calculus?What is a desugarer?What is a first order variable?What is a fresh renaming?What is a fresh variable (concerning a set of variables)?What is a general judgment?What is a generic inductive definition?What is a hypothesis in the context of hypothetical judgments?What is a hypothetical entailment?What is a hypothetical rule?What is a lexicographic order What is a local binding form?What is a logical system?What is a macro?What is a macro system?What is a metalanguage?What is a metatheory?What is a metavariable?What is a normal form?What is a partial order?What is a powerset?What is a preorder?What is a primordial block in programming language?What is a program in grammar?What is a redex or reducible expression in church What is a rule schema and its relation with concrete rules?What is a rule scheme?What is a tactic in rocq?What is a term in grammar?What is a value in programming language calculus?What is admissibility as a notion of entailment?What is aliasing?What is an abstract binding graph (ABG)?What is an abstract binding tree (ABT)?What is an axiom (inference rule)?What is an environment in programming language?What is an equivalence?What is an equivalent way of defining $J_1, \dots, J_n \vdash_{\mathcal{R}} J$?What is an evaluation strategy?What is an evaluator?What is an example for the tradeoffs between the type system What is an example of a generic derivation?What is an instance of an inference rule?What is an intro pattern in rocq?What is an object?What is an object language?What is an REPL?What is another name for the divergent combinator?What is automatic memory management?What is beta reduction?What is BNF?What is church numerals?What is derivability as a notion of entailment?What is garbage collection?What is generic derivability judgment defined by?What is governance?What is language safety, both formally and informally?What is lexical/static scope?What is macro expansion?What is meta-mathematics?What is notation scope in rocq? how to explicitly specify them?What is operational semantics?What is parallel/simultaneous let?What is proof by case analysis in rocq?What is proof by rewriting in rocq?What is proof by simplification in rocq?What is recursive let?What is rocq?What is sequential let?What is structural induction?What is the assignment operator in rocq?What is the class pattern?What is the class pattern with both private members and static members?What is the class pattern with private members?What is the deduction style presentation of logical systems?What is the definition of the fixed-point combinator?What is the destruct tactic in rocq?What is the difference between a compiler and an interpreter?What is the difference between a formal derivability judgment and a derivability judgment?What is the difference between a formal generic judgment and a generic judgment?What is the difference between = and =? in rocq?What is the difference between formal and actual parameters?What is the difference between the implicit and explicit form of a generic rule in a generic inductive definition?What is the divergent combinator?What is the evaluation relation?What is the expression problem?What is the forall keyword in rocq?What is the form of a generic rule?What is the formal definition for alpha-equivalence?What is the fundamental requirement of rocq on its argument of a fixpoint definition?What is the Hindley-Milner type inference algorithm?What is the idea of hypothetical inductive definition?What is the idea of JIT compilation?What is the idea of mixins?What is the idea of traits?What is the inductive definition of a judgment form?What is the kernel of the rocq system?What is the main principle of functional programming?What is the meaning of a term?What is the meaning of the of the notation $gamma dash^{mathcal{u};mathcal{x}}_mathcal{r}j$?What is the motivation for hypothetical inductive definitions?What is the name of rocq What is the object pattern?What is the one-step evaluation relation?What is the operational semantics of arithmetic expressions?What is the operational semantics of boolean expressions?What is the portability perspective on language safety?What is the principle of mathematical induction?What is the principle of tree induction?What is the relation between basic objects and lambdas?What is the relation between language safety and partiality?What is the relation between macros and parenthetical language?What is the relation between "meaning" and "representation"?What is the relation between methods and functions?What is the relation between objects and closures?What is the relation between types and runtime values?What is the relationship between a generic inductive definition and an ordinary inductive definition?What is the rewrite tactic in rocq?What is the shorthand for the pattern intros then immediately destruct the same variable? what is its downside?What is the syntax for conditional expressions in rocq?What is the syntax for imports in rocq?What is the syntax for multi-argument application in rocq?What is the technique of induction on derivations?What is the untyped calculus of booleans and numbers?What is the usual treatment for the substitution problems (variable capture, etc.)What is the wildcard pattern in rocq?What is usually meant by substitution?What is usually used as a state for the abstract machine in operational semantics?What kinds of languages in which parametric judgments are required to specify?What makes a type system sound?What some structural properties of derivability?What to consider about the interaction between macros and side effects?What What What What What What What What What What What What What What What What What What What What When a rule is not an axiom, what is it called?When do we call an evaluation statement is derivable?When is a rule satisfied by a relation?Where can operators (in a bob harper Where can variables be placed in an AST?Which desirable properties should hold for most systems, which would not?Which evaluation strategies are strict/lazy?Which form of hypothetical judment is stronger, admissibility or derivability? why?Which notation is often used to denote a preorder relation?Which notation is often used to denote strict inequality in preorder?Which notations are usually used to specify sets?Which programming paradigm is a bridge between programming and logic?Which special treatments are given to natural numbers in rocq?Which symbol is used to denote an evaluation result of a term?Which symbol is used to denote enriched lambda calculus with numbers and booleans?Which symbol is used to denote pure lambda calculus?Which symbol is usually used to denote subtyping relation?Which symbols are usually given to a finite set of basic judgments?Which symbols can be used to mark nested subgoals in destruct in rocq?Which terms are deemed values in untyped lambda calculus?Which types are supported in conditional expressions Which values are truthy in rocq?Why are most dynamically checked languages safe?Why are type systems a valuable maintenance tool?Why can there be nonsensical terms in the untyped calculus of booleans and numbers?Why can type checkers be viewed as extended parsers?Why did lambda calculus see widespread use in programming language specification, type system studies, etc?Why does matklad think mod.rs-less system is self-inconsistent?Why does type inference cause vague error messages?Why does we require rules in a hypothetical inductive definition be uniform? what does it mean to be uniform?Why is backward chaining goal-directed?Why is forward chaining undirected?Why is it useful to give >= 2 operational semantics for a single language?Why is self-application impossible to typed?Why is subclass = subtype a controversial choice?Why is the admissibility judgment not stable under extension to the rules?Why is the derivability judgment stable under extension to the rules?Why is the property that static types are checked at compile-time is valuable?Why is there a need for macro hygiene?Why is there a need for syntactic sugar?Why is union type popular in retrofitted type systems?Why should language design go hand in hand with type system design?