This lecture introduces Amyli, a tiny functional language supporting recursive functions, with an abstract syntax for terms and operational semantics. It covers the execution of programs, type rules, and soundness through progress and preservation, including proofs and examples.