목록전체 글 (110)
strangerRidingCaml
Introduction to Inference Rules and Typing Rules Inference rules and typing rules are fundamental components of formal systems used to derive conclusions about the behavior and properties of expressions. Inference rules are logical rules that specify how new knowledge or conclusions can be derived from existing premises or assumptions. They are typically expressed as a set of premises leading..
Simply Typed Lambda Calculus (STLC) The Simply Typed Lambda Calculus (STLC) is a foundational formal system in lambda calculus with typed expressions. In STLC, each lambda abstraction is annotated with a specific type, and the application of functions is type-checked to ensure type compatibility. The syntax of STLC includes terms, types, and typing judgments. Terms are represented as lambda ..
Basic Concepts of Type Theory In Type Theory, types are fundamental constructs that classify various entities in a formal system. Each entity, known as a term, is assigned a type, indicating its nature or category. Terms represent objects, values, or expressions within the system, while types categorize these terms based on their properties. For example, in a simple type system, we might hav..
Overview of Type Theory: Historical Context and Motivation Type Theory is a foundational framework in mathematics and computer science for formalizing the notion of computation and reasoning about types of data. The roots of Type Theory can be traced back to the early 20th century, with the work of David Hilbert and Alonzo Church. In the 1930s, Church introduced the concept of the lambda calc..
Advanced Topics in Software VerificationModel-driven engineering and formal methodsModel-driven engineering (MDE) is an approach to software development that emphasizes the use of models as primary artifacts throughout the development lifecycle. Formal methods are mathematical techniques used to specify, develop, and verify software systems. MDE and formal methods complement each other, as forma..
Model Checking and Automated VerificationIntroduction to model checking techniquesModel checking is a formal verification technique used to check whether a system satisfies a given property by exhaustively exploring all possible states of the system. It involves constructing a finite-state model of the system and verifying properties of interest by systematically exploring the state space and ch..