Difference between revisions of "IU:TestPage"

From IU
Jump to navigation Jump to search
Line 1: Line 1:
   
  +
= -Calculus, Algebra, Machinery and Logic for Formal Program Semantics =
−
= Course design in STEM in Higher Education =
  
−
* '''Course name''': Course design in STEM in Higher Education
 +
* '''Course name''': -Calculus, Algebra, Machinery and Logic for Formal Program Semantics
−
* '''Code discipline''': ???
 +
* '''Code discipline''': CSE835
−
* '''Subject area''': Humanities
 +
* '''Subject area''': Software Engineering
   
 
== Short Description ==
  
== Short Description ==
  +
This elective course is designed for students in Computer Science, Software Engineering (IT more generally) and in Mathematics to catch main concepts formal program semantics and basic ideas from formal program specification and verification. We start with a make easy approach to formal semantics based on a toy language with esoteric operational, denotational, and logical (axiomatic) semantics. Then we move to operational, denotational, and axiomatic semantics for a simple imperative programming language.
−
This course is meant to guide you through the process of designing an elective course that you can potentially teach at Innopolis University. The transferable skills you should acquire within this course are (1) to be able to consciously make educated pedagogical decisions related to essential aspects of course design in higher education - the course design process as well as setting up course level objectives and aligning with them assessments, course content, and instructional practices; (2) to be able to document those decisions as a syllabus.
  
   
 
== Prerequisites ==
  
== Prerequisites ==
   
 
=== Prerequisite subjects ===
  
=== Prerequisite subjects ===
  +
* CSE101, CSE102, CSE103, CSE104, CSE109
−
* HSS104
  
  +
* CSE110 or CSE111 or CSE113 or CSE116
  +
* CSE117, CSE119
   
 
=== Prerequisite topics ===
  
=== Prerequisite topics ===
  +
* natural, integer, rational, and real numbers
−
* Bloom et al.’s taxonomy
  
  +
* functions and relations on numbers
−
* constructive alignment
  
  +
* axiomatic method in geometry
  +
* imperative (procedural) programming and languages
  +
* algorithm complexity theory and data structures
  +
* regular and context-free grammars and languages
  +
* finite state machines (automata)
  +
* basic programming skills
  +
* basics of OOP software design
  +
* familiarity with some development framework or technology (web or mobile)
   
 
== Course Topics ==
  
== Course Topics ==
Line 23: Line 33:
 
! Section !! Topics within the section
  
! Section !! Topics within the section
 
|-
  
|-
  +
| Section I: Course intro and Recall ||
−
| Setting course objectives. ||
 
  +
# Course Intro, Recall from Discrete Mathematics and home asynchronous evaluation test on naïve set theory, algebra of binary relations, propositional logic, basics of programming paradigms
−
# Course design frameworks
  
−
# Needs assessment
  
−
# International, national, institutional, occupational curricula
  
−
# Assessment
  
 
|-
  
|-
  +
| Section II: Introduction to Program Semantics ||
−
| Instruction. ||
 
  +
# Introduction to Program Semantics:
−
# Scholarship of teaching and learning
  
  +
# What is Semantics? Why Formal Program Semantics?
−
# Learning theories
  
  +
# Operational, denotational, and axiomatic semantics for esoteric language
−
# Teaching and learning approaches
  
−
# Ethical considerations and inclusive teaching
  
−
# Materials design
  
−
# Teaching practice
  
 
|-
  
|-
  +
| Section III: Formal semantics for a simple imperative programming language ||
−
| Documentation. ||
 
  +
# Formal semantics for a simple imperative programming language
−
# Syllabus design
  
  +
# Data Types and Their Semantics
−
# Teaching philosophy statement
  
  +
# The main ingredient: Implementation Semantics
  +
# Structural Operational Semantics (SOS)
  +
# Relational denotational semantics
  +
# Axiomatic semantics
  +
# Elements of deductive program verification
  +
|-
  +
| Section IV: <br>λ-Calculus and Classical Denotational Semantics ||
  +
# λ-Calculus and Classical Denotational Semantics
  +
# Syntax, semantics, and main properties of λ-Calculus
  +
# Denotational semantics of a simple imperative programming language
  +
|-
  +
| Section V:<br>Typed λ-Calculus and semantics of a simple functional language ||
  +
# System F and its applications
  +
# Introduction of polymorphic λ-Calculus
  +
# Curry–Howard isomorphism and the Lambda Cube
  +
# Use in programming languages
 
|}
 
|}
 
== Intended Learning Outcomes (ILOs) ==
  
== Intended Learning Outcomes (ILOs) ==
Line 45: Line 65:
 
=== What is the main purpose of this course? ===
  
=== What is the main purpose of this course? ===
 
What is the main goal of this course formulated in one sentence?
  
What is the main goal of this course formulated in one sentence?
−
The main purpose of this course is to enable students to design a university elective course.
 +
The main purpose of the course is to introduce the modern theory of programming languages.
   
 
=== ILOs defined at three levels ===
  
=== ILOs defined at three levels ===
Line 51: Line 71:
 
==== Level 1: What concepts should a student know/remember/explain? ====
  
==== Level 1: What concepts should a student know/remember/explain? ====
 
By the end of the course, the students should be able to ...
  
By the end of the course, the students should be able to ...
  +
* why we need formal semantics for programming languages
−
* describe several course design frameworks and judge their applicability;
  
  +
* principles of operational, denotational, and axiomatic approaches to formal semantics
−
* explain the purpose of needs assessment and describe the steps of the process;
  
  +
* how to use of formal semantics for static analysis and formal verification
−
* explain the difference between knowledge-based and competency-based course design approaches;
  
−
* characterize national, international, and occupational (CS2020) curricula;
  
−
* give examples of program level competencies – universal, general professional, professional;
  
−
* explain the concepts of alignment, sequencing, progression, and recycling related to course design;
  
−
* list and describe the learning theories you know;
  
−
* list and describe teaching and learning approaches you know;
  
−
* describe how ethical and inclusive teaching issues should be considered during the course design;
  
−
* explain the concepts of alignment, progression, and recycling;
  
−
* give examples of different forms of syllabi and explain their purposes;
  
−
* explain the purpose of a teaching philosophy statement and give examples of the content relevant for this document.
  
   
 
==== Level 2: What basic practical skills should a student be able to perform? ====
  
==== Level 2: What basic practical skills should a student be able to perform? ====
 
By the end of the course, the students should be able to ...
  
By the end of the course, the students should be able to ...
  +
* define a operational, donotational, and axiomatic semantics for a simple imperative and functional programming language
−
* design course level competency statements in line with CS2020 curriculum;
  
  +
* to specify formally and verify manually simple computational programs on a simple imperative or functional language.
−
* describe the intended learning outcomes of the course;
  
−
* align course level objectives with national, occupational, and institutional curricula;
  
−
* align the course ILOs with assessment and instruction;
  
−
* design course materials;
  
−
* design formative and summative assessment tasks aligned with the competency statement
  
   
 
==== Level 3: What complex comprehensive skills should a student be able to apply in real-life scenarios? ====
  
==== Level 3: What complex comprehensive skills should a student be able to apply in real-life scenarios? ====
 
By the end of the course, the students should be able to ...
  
By the end of the course, the students should be able to ...
  +
* problems with developing formal semantics for industrial programming languages.
−
* perform needs assessment and write up results;
  
  +
* use of formal semantics for static analysis and formal verification.
−
* design and teach a 45’ class on their own where content, instruction, and assessment are mutually aligned and aligned with the competency statement;
  
  +
* ways of introduction of formal semantics into Software engineering practice.
−
* write up a course syllabus;
  
−
* justify their pedagogical choices based on research-based evidence.
 
 
== Grading ==
  
== Grading ==
   
Line 87: Line 93:
 
! Grade !! Range !! Description of performance
  
! Grade !! Range !! Description of performance
 
|-
  
|-
−
| A. Excellent || 95.0-100.0 || -
 +
| A. Excellent || 85.0-100.0 || -
 
|-
  
|-
−
| B. Good || 80.0-94.99 || -
 +
| B. Good || 75.0-84.0 || -
 
|-
  
|-
−
| C. Satisfactory || 70.0-79.99 || -
 +
| C. Satisfactory || 65.0-74.0 || -
 
|-
  
|-
−
| D. Fail || 0.0-69.99 || -
 +
| D. Fail || 0.0-64.0 || -
 
|}
  
|}
   
Line 102: Line 108:
 
! Activity Type !! Percentage of the overall course grade
  
! Activity Type !! Percentage of the overall course grade
 
|-
  
|-
  +
| Home-made problem-solving assignments for each of 5 sections of the course (10points for each assignment) || 50
−
| Needs assessment || 10
  
 
|-
  
|-
  +
| Individual in-class participation based on work in class (1 point for each class) || 10
−
| Participation || 25
  
 
|-
  
|-
  +
| Final home-made written asynchronous examination || 40
−
| Class analysis || 40
  
−
|-
  
−
| Thinking behind your course || 10
  
−
|-
  
−
| Syllabus || 10
  
−
|-
  
−
| Course presentation || 5
  
 
|}
  
|}
   
 
=== Recommendations for students on how to succeed in the course ===
  
=== Recommendations for students on how to succeed in the course ===
  +
In-class participation is important (it implies attendance importance).<br>Topic-based regular home-made assignment are major grading item.<br>Please be aware that the lecture materials cover a plenty of topics from many sources, not a single one.
−
Participation and self-study are important.<br>You will benefit from discussing the course readings.
  
   
 
== Resources, literature and reference materials ==
  
== Resources, literature and reference materials ==
   
 
=== Open access resources ===
  
=== Open access resources ===
  +
* Dijkstra E.W. A Discipline of Programming. Prentice-Hal, 1976.
−
* Fink, L. D. (2003). A self-directed guide to designing courses for significant learning. Retrieved from http://www.deefinkandassociates.com/ GuidetoCourseDesignAug05.pdf
  
  +
* Gries D. The Science of Programming. Springer, 1987.
−
* CC2020 Task Force. 2020. Computing Curricula 2020: Paradigms for Global Computing Education. Association for Computing Machinery, New York, NY, USA.
  
  +
* Aaby A. Introduction to Programming Language. Working draft, 2004. Available at .
−
* Bates, A.W. (2015)  Vancouver BC: Tony Bates Associates Ltd. ISBN: 978-0-9952692-0-0.
  
  +
* Barendregt H. Lambda Calculi with Types. In: Handbook of Logic in Computer Science. Oxford University Press, 1992. Vol. II, pp. 117-309. Available at ftp://ftp.cs.ru.nl/pub/CompMath.Found/HBK.ps.
  +
* Shilov N.V. Introduction to Program Syntax, Semantics and Verification. (In Russian.) Novosibirsk State University, 2011. Draft is available at .
   
 
=== Closed access resources ===
  
=== Closed access resources ===
  +
* Not needed.
−
* Teaching and Learning STEM: A Practical Guide, Richard M. Felder and Rebecca Brent. Jossey-Bass—A Wiley Brand: San Francisco, CA, 2016. ISBN: 978-1-118-92581-2
  
−
* Race, P. (2019). The Lecturer's Toolkit: A Practical Guide to Assessment, Learning and Teaching (5th ed.). Routledge.
  
−
* Biggs, J. B., & Tang, C. (2011). Teaching for quality learning at university (4th ed.). Open University Press.
  
   
 
=== Software and tools used within the course ===
  
=== Software and tools used within the course ===
  +
* Any compiler and IDE to implement, test, and exercise simple computational, search and sorting imperative and functional algorithms/programs.
−
* Provide at least 3 open/freemium access tools
  
−
* None
 
 
= Teaching Methodology: Methods, techniques, & activities =
  
= Teaching Methodology: Methods, techniques, & activities =
   
 
== Activities and Teaching Methods ==
  
== Activities and Teaching Methods ==
 
{| class="wikitable"
  
{| class="wikitable"
−
|+ Activities within each section
 +
|+ Teaching and Learning Methods within each section
 
|-
  
|-
−
! Learning Activities !! Section 1 !! Section 2 !! Section 3
 +
! Teaching Techniques !! Section 1 !! Section 2 !! Section 3 !! Section 4 !! Section 5
 
|-
  
|-
  +
| Problem-based learning (students learn by solving open-ended problems without a strictly defined solution) || 1 || 1 || 1 || 1 || 1
−
| Interactive Lectures || 1 || 1 || 1
  
 
|-
  
|-
  +
| Differentiated learning (provide tasks and activities at several levels of difficulty to fit students needs and level) || 1 || 1 || 1 || 1 || 1
−
| Lab exercises || 1 || 1 || 1
  
 
|-
  
|-
  +
| Contextual learning (activities and tasks are connected to the real world to make it easier for students to relate to them); || 1 || 1 || 1 || 1 || 1
−
| Individual Projects || 1 || 1 || 1
  
  +
|-
  +
| Развивающее обучение (задания и материал "прокачивают" ещё нераскрытые возможности студентов); || 1 || 1 || 1 || 1 || 1
  +
|-
  +
| Концентрированное обучение (занятия по одной большой теме логически объединяются); || 1 || 1 || 1 || 1 || 1
  +
|}
  +
{| class="wikitable"
  +
|+ Activities within each section
 
|-
  
|-
  +
! Learning Activities !! Section 1 !! Section 2 !! Section 3 !! Section 4 !! Section 5
−
| Flipped classroom || 1 || 1 || 1
  
 
|-
  
|-
−
| Peer Review || 1 || 1 || 1
 +
| Lectures || 1 || 1 || 1 || 1 || 1
 
|-
  
|-
−
| Discussions || 1 || 1 || 1
 +
| Interactive Lectures || 1 || 1 || 1 || 1 || 1
 
|-
  
|-
−
| Presentations by students || 1 || 1 || 1
 +
| Lab exercises || 1 || 1 || 1 || 1 || 1
 
|-
  
|-
−
| Written reports || 1 || 1 || 1
 +
| Flipped classroom || 1 || 1 || 1 || 1 || 1
 
|-
  
|-
−
| Oral Reports || 1 || 1 || 1
 +
| Quizzes (written or computer based) || 1 || 1 || 1 || 1 || 1
 
|-
  
|-
−
| Experiments || 0 || 0 || 1
 +
| Discussions || 1 || 1 || 1 || 1 || 1
 
|}
 
|}
 
== Formative Assessment and Course Activities ==
  
== Formative Assessment and Course Activities ==
Line 171: Line 177:
 
! Activity Type !! Content !! Is Graded?
  
! Activity Type !! Content !! Is Graded?
 
|-
  
|-
  +
| Home-made problem-solving assignment || Assume that , , and are sets. <br>Prove without use of the power-set axiom that is a set.<br>Prove without use of the set-union axiom that is a set.<br>Prove (using extensionality postulate) <br>uniqueness of the empty set<br>uniqueness of the set for any given finite collection of sets of , … .<br>Proof (using the enumeration and union postulate) existence of the standard union for all sets and . <br>Proof (using the specification postulate) existence of the standard intersection for all sets and .<br>Prove that for any set and any its subset the complement is a set.<br>Proof (by contradiction using specification axiom) that collection usually called as the set of all sets isn’t a set. (Russel’s paradox.) || 1
−
| Needs assessment || Compare and contrast three course design frameworks: ADDIE, SAM, Integrated course design. <br>List the stages you will take to design your course.<br>Design a plan to perform needs assessment. || 0
  
−
|-
  
−
| Thinking behind your course || Document the following sections of the portfolio (“Thinking behind your course”):<br>Situational factors<br>Program level objectives<br>Competency statement <br>Assessment || 0
  
 
|}
 
|}
 
==== Section 2 ====
  
==== Section 2 ====
Line 181: Line 185:
 
! Activity Type !! Content !! Is Graded?
  
! Activity Type !! Content !! Is Graded?
 
|-
  
|-
  +
| Home-made problem-solving assignment || Is TEL a regular language? A context-free language? A context-sensitive language? A Recursively enumerable language? <br>What will happen with TEL syntax (in terms of Chomsky classification) if it adopts spacing and indentation like Python?<br>Assuming that all variables are of integer type and a conventional semantics for program answer what does this program compute?<br>Validate that is indeed the operational semantics of TEL sentence .<br>Prove that in TEL the following sentences and are equivalent.<br>Prove that and are not equivalent in TEL. || 1
−
| Learning theories and teaching and learning approaches || Compare and contrast the following learning theories: behaviorism, cognitivism, constructivism, connectivism.<br>Describe and critically evaluate the following teaching and learning approaches: project-based learning, problem-based learning, case-based learning, just-in-time teaching, process oriented guided inquiry learning (POGIL), studio-based learning, universal design for learning.<br> Which of the learning theories and teaching and learning approaches reflect your teaching philosophy? || 0
  
  +
|}
  +
==== Section 3 ====
  +
{| class="wikitable"
  +
|+
 
|-
  
|-
  +
! Activity Type !! Content !! Is Graded?
−
| Ethical considerations and inclusive teaching. || Explain how instructional and materials design should consider the special needs of color-blind, dyslectic, dysgraphic, intellectually advanced, and culturally diverse students.<br> || 0
  
 
|-
  
|-
  +
| Home-made problem-solving assignment || Is ToyPL-VM language a context-free? Does it have a context-free syntax? <br>Assuming a conventional program semantics and that the only data type is mathematical integers, try to guess (and prove somehow) what does compute the following ToyPL-VM program:<br>0: if z<0 then 1 else 2; <br>1: z:= -1 goto 8; <br>2: x:= 0 goto 3; <br>3: y:= 0 goto 4; <br>4: if y≤z then 5 else 7; <br>5: y:= y+2*x+1 goto 6; <br>6: x:= x+1 goto 4; <br>7: x:= x-1 goto 8;<br>Let be any ToyPL-VM program, be any state of . Define by induction on structure of the expression (that uses variables in only) the value of this expression in this state . <br>Let be any ToyPL-VM program, be any state of . Prove by induction on structure of the expression that for any expression (based on variables in ) the value of this expression in this state has a definite value.<br>Validate that the implementation (semantics) of the ToyPL program from the left column is the ToyPL-VM program in right column.<br>Select (always) valid assertions and explain your choice:<br> || 1
−
| Teaching practice. || Plan, design materials, and teach a 45’ pilot class for BS students.<br>Participate in your classmates’ class as a student or as an observer. <br>Document your reflection about your class.<br>Document and present your feedback for your classmates’ classes. || 1
  
  +
|}
  +
==== Section 4 ====
  +
{| class="wikitable"
  +
|+
 
|-
  
|-
  +
! Activity Type !! Content !! Is Graded?
−
| Scholarship of teaching and learning || Read and summarize one of the provided articles, post your summary on the forum.<br>Discuss the articles with your classmates. Explain how what you have read can impact your pedagogical choices. || 1
  
 
|-
  
|-
  +
| Home-made problem-solving assignment || Is the language of the -Calculus regular? Context-free?<br>The following sugared -term is representation of the following -term:<br><br><br><br><br><br>List all free and bound variable instances in the -terms (a)-(e) from the previous exercise. Which of these -terms are combinators?<br>Assuming the sugaring has no precedence, whether the desugaring of the -terms is confluent (i.e., always end with the same term)?<br>Assuming the sugaring has the specified precedence, whether the desugaring of the -terms is confluent (i.e., always end with the same term)?<br>Explain the following “proof” in the axiomatic semantics of the -Calculus and find a breach of the semantics:<br> || 1
−
| Thinking behind your course || Document the following sections of the portfolio (“Thinking behind your course”):<br>Learning theory your course draws upon. Give example of learning experiences your students will be exposed to that are aligned with the vision of that learning theory.<br>Teaching and learning approach your course draws upon. Give example of learning experiences your students will be exposed to that are aligned with those approaches.<br>Ethical and inclusive teaching issues you should consider while designing your course and materials. <br>How learning will happen in your course.<br>List the topics that will be covered and how they will be sequenced.<br>Explain the progression within the course – how the students will be challenged during the course.<br>Explain which concepts will be recycled within the course.<br>Explain how the course competency statement, ILOs, assessments, and instruction are mutually aligned in the course. <br>Anticipate the potential risks in the course and plan how you can overcome them. <br> || 0
  
 
|}
 
|}
−
==== Section 3 ====
 +
==== Section 5 ====
 
{| class="wikitable"
  
{| class="wikitable"
 
|+
 
|+
Line 197: Line 209:
 
! Activity Type !! Content !! Is Graded?
  
! Activity Type !! Content !! Is Graded?
 
|-
  
|-
  +
| Home-made problem-solving assignment || Suggest any fix-point combinator other than .<br>Write a Java-, Python-, etc. program that (being aware about its location) prints out its own code.<br>Write yourself a quine-program in Java, Python, etc. <br>Give example of a -term such that has a reduction graph that<br>is a singleton with a single edge <br>is a finite chain of length <br>is an infinite chain<br>Prove Church-Rosser theorem: If there are two distinct (-)reductions starting from a -term, then there exists a -term that is reachable from both reducts via a (possibly empty) sequence of (-)reductions.<br>What is true:<br>If a -term has a normal form, then its reduction graph is finite.<br>If a -term has a finite reduction graph, then it has a normal form.<br>Proof by induction of the height of the inference tree soundness of the axiomatic semantic of -Calculus: For any -terms and , if then there exists -term such that and . || 1
−
| Syllabus || Write up a draft of the syllabus of your course using the provided template. || 0
  
−
|-
  
−
| Teaching philosophy statement || Write a draft of your teaching philosophy statement. || 1
  
 
|}
 
|}
 
=== Final assessment ===
  
=== Final assessment ===
 
'''Section 1'''
  
'''Section 1'''
  +
# Can be a final exam, project defense, or some other equivalent of the final exam.
−
# Grading criteria for the Needs assessment report:
  
  +
# The final examination is distance asynchronous individual written test to check that students understand and can apply main definitions, concepts and techniques presented on the lectures and available in lecture notes. The main grading criterions for written test will be human readable but concise, self-completeness, well-structuredness, and “proof of individual work” while computational (mainly arithmetic) errors will be treated as tiny mistakes (at most one-point deduction for each individual task).
−
# The work shows the evidence of thorough planning and performing research. The plan was timely designed as per which data need to be collected, the ways to collect them and to analyze them. Several, where possible, representatives/groups of representatives of each of the types of stakeholders (industry, students, University) have been interviewed. Other data were collected if necessary. The collected data provide solid evidence to justify the choices of the course content and mode of delivery.
  
  +
# Examination has one (parameterized) variant for all enrolled students with 5 tasks with cost 8 points each (i.e., 40 points in total). “Human readable but concise” rule means that solutions should be well-commented but not exciding 1.5 (one and a half) pages each. Self-completeness means that the paper should be readable independently on any other resource, but lecture notes. Well-structuredness means that each task formulation, solution (proof if needed), answer (or conclusion) and its parts must be explicit in the paper and identified by appropriate headings/keywords (with respect to logical structure).
  +
# Sample tasks follow.
  +
# Task 1. Using definition of the natural number as in the lecture notes for section 1, construct the powerset for a given (specified) natural number . How many elements does it (the powerset) contains? (Explain all your answers.)
  +
# Task 2. Using definitions from the lecture notes for section 2, construct a TEL “meaningful program” that after evaluation according to TEL informal semantics gets value , construct (step by step) its operational, denotational, and axiomatic semantics according to the TEL definitions. Here “meaningful” means that you can explain what does the program computes assuming a conventional informal program semantics. Please explain informally what this semantics is.
  +
# Task 3. Using definitions from the lecture notes for section 3, and the same program as you construct in the exercise 2 above, construct (step by step) its operational and denotational semantics as a ToyPL program.
  +
# Task 4. Using definitions from the lecture notes for section 3, and the same program as you construct in the exercise 2 above, specify the program by pre- and post-conditions according to your explanations (in the exercise 2) of what does the program compute, and then verify (using Floyd method or Hoare axiomatic semantics) correctness of the specified program.
  +
# Task 5. Using definitions from the lecture notes for sections 4 & 5, construct a given (specified) natural number . Whether it is a combinator? Build reduction graph for . (Explain all your answers.)
 
'''Section 2'''
  
'''Section 2'''
  +
−
# none
  
 
'''Section 3'''
  
'''Section 3'''
  +
−
# Grading criteria for the course syllabus, course development portfolio, and presentation:
  
  +
'''Section 4'''
−
# The work is a result of incremental documentation of the vision of the course developer of the situational factors, course objectives, instruction, feedback and assessment, potential risks, and evaluation of the course. The work demonstrates that the course designer makes their pedagogical decisions consciously and responsibly and based on the research evidence where possible; proper explanations and examples are provided to justify those choices. The course designer demonstrates excellent knowledge of learning theories and instructional approaches and full understanding of the concepts of alignment/integration, progression, and recycling.
  
  +
  +
'''Section 5'''
  +
   
 
=== The retake exam ===
  
=== The retake exam ===
 
'''Section 1'''
  
'''Section 1'''
  +
# Retake and re-examinations are designed to check that students understand and can apply main definitions, concepts and techniques covered in the lectures of the Course to overwrite grades for the final examination.
−
# For the retake, students must submit course syllabus and present their course design portfolio.
  
  +
# Hybrid re-examination mode means that the examinations comprise a distance asynchronous individual written test (the first re-examination to be graded by Prof. N.V. Shilov) and an oral defense in front of a commission (consisting of Prof. N.V. Shilov and two more faculty to be appointed by the time of the second re-examination); format of the oral defense – offline or online – to be decided/arranged later (but prior to the defense date to be set by the Department of Education).
  +
# Since (according to the Syllabus available the final examination costs 40 points, the cost of the re-examination is also 40 points. So, individual overall grade for the course after the retake for each participating student will be calculated according to the following formula , where is student’ overall score earned for the course during the teaching term, is student’ overall score earned for the final examination, is student’ score earned for the re-examination.
  +
# Examination set comprises 5 individual tasks (but the same for both retakes) with cost points each (i.e., 40 points in total). “Human readable but concise” rule means that solutions should be well-commented but not exciding 1.5 (one and a half) pages each. Self-completeness means that the paper should be readable independently on any other resource, but lecture notes. Well-structuredness means that each task formulation, solution (proof if needed), answer (or conclusion) and its parts must be explicit in the paper and identified by appropriate headings/keywords (with respect to logical structure).
  +
# Sample tasks follow.
  +
# Task 1. Let us assume that ‘’, ‘‘, ‘’, and ‘’ are symbols. Using definition of the natural number as in the lecture notes on the topic 1, count (ignoring blank spaces) the length of the string thar represents a given natural number . How many elements does this representation contains? (Explain all your answers.)
  +
# Task 2. Using definitions from the lecture notes on the topic 2, construct a TEL-program that in conventional (natural for a programming language) semantics computes (outputs) the integer part of the square root of a (input) positive integer, but that after evaluation according to TEL informal semantics gets value for a given natural number , construct (step by step) its operational, denotational, and axiomatic semantics according to the TEL definitions.
  +
# Task 3. Using definitions from the lecture notes on the topic 3, and the same program as you construct in the exercise 2 above, construct (step by step) its implementation and denotational semantics as a ToyPL program.
  +
# Task 4. Using definitions from the lecture notes on the topic 3, and the same program as you construct in the exercise 2 above, specify the program by pre- and post-conditions according to your explanations (in the exercise 2) of what does the program compute, and then verify (using Floyd method or Hoare axiomatic semantics) correctness of the specified program.
  +
# Task 5. Using definitions from the lecture notes on the topics 4 and 5, construct explicitly the numeral for a given natural number . What is type of the numeral Demonstrate that . What is type of the term ? Build reduction graph for . (Explain all your answers.)
 
'''Section 2'''
  
'''Section 2'''
   
 
'''Section 3'''
  
'''Section 3'''
  +
  +
'''Section 4'''
  +
  +
'''Section 5'''

Revision as of 13:50, 9 February 2023

-Calculus, Algebra, Machinery and Logic for Formal Program Semantics

  • Course name: -Calculus, Algebra, Machinery and Logic for Formal Program Semantics
  • Code discipline: CSE835
  • Subject area: Software Engineering

Short Description

This elective course is designed for students in Computer Science, Software Engineering (IT more generally) and in Mathematics to catch main concepts formal program semantics and basic ideas from formal program specification and verification. We start with a make easy approach to formal semantics based on a toy language with esoteric operational, denotational, and logical (axiomatic) semantics. Then we move to operational, denotational, and axiomatic semantics for a simple imperative programming language.

Prerequisites

Prerequisite subjects

  • CSE101, CSE102, CSE103, CSE104, CSE109
  • CSE110 or CSE111 or CSE113 or CSE116
  • CSE117, CSE119

Prerequisite topics

  • natural, integer, rational, and real numbers
  • functions and relations on numbers
  • axiomatic method in geometry
  • imperative (procedural) programming and languages
  • algorithm complexity theory and data structures
  • regular and context-free grammars and languages
  • finite state machines (automata)
  • basic programming skills
  • basics of OOP software design
  • familiarity with some development framework or technology (web or mobile)

Course Topics

Course Sections and Topics
Section Topics within the section
Section I: Course intro and Recall
  1. Course Intro, Recall from Discrete Mathematics and home asynchronous evaluation test on naïve set theory, algebra of binary relations, propositional logic, basics of programming paradigms
Section II: Introduction to Program Semantics
  1. Introduction to Program Semantics:
  2. What is Semantics? Why Formal Program Semantics?
  3. Operational, denotational, and axiomatic semantics for esoteric language
Section III: Formal semantics for a simple imperative programming language
  1. Formal semantics for a simple imperative programming language
  2. Data Types and Their Semantics
  3. The main ingredient: Implementation Semantics
  4. Structural Operational Semantics (SOS)
  5. Relational denotational semantics
  6. Axiomatic semantics
  7. Elements of deductive program verification
Section IV:
λ-Calculus and Classical Denotational Semantics
  1. λ-Calculus and Classical Denotational Semantics
  2. Syntax, semantics, and main properties of λ-Calculus
  3. Denotational semantics of a simple imperative programming language
Section V:
Typed λ-Calculus and semantics of a simple functional language
  1. System F and its applications
  2. Introduction of polymorphic λ-Calculus
  3. Curry–Howard isomorphism and the Lambda Cube
  4. Use in programming languages

Intended Learning Outcomes (ILOs)

What is the main purpose of this course?

What is the main goal of this course formulated in one sentence? The main purpose of the course is to introduce the modern theory of programming languages.

ILOs defined at three levels

Level 1: What concepts should a student know/remember/explain?

By the end of the course, the students should be able to ...

  • why we need formal semantics for programming languages
  • principles of operational, denotational, and axiomatic approaches to formal semantics
  • how to use of formal semantics for static analysis and formal verification

Level 2: What basic practical skills should a student be able to perform?

By the end of the course, the students should be able to ...

  • define a operational, donotational, and axiomatic semantics for a simple imperative and functional programming language
  • to specify formally and verify manually simple computational programs on a simple imperative or functional language.

Level 3: What complex comprehensive skills should a student be able to apply in real-life scenarios?

By the end of the course, the students should be able to ...

  • problems with developing formal semantics for industrial programming languages.
  • use of formal semantics for static analysis and formal verification.
  • ways of introduction of formal semantics into Software engineering practice.

Grading

Course grading range

Grade Range Description of performance
A. Excellent 85.0-100.0 -
B. Good 75.0-84.0 -
C. Satisfactory 65.0-74.0 -
D. Fail 0.0-64.0 -

Course activities and grading breakdown

Activity Type Percentage of the overall course grade
Home-made problem-solving assignments for each of 5 sections of the course (10points for each assignment) 50
Individual in-class participation based on work in class (1 point for each class) 10
Final home-made written asynchronous examination 40

Recommendations for students on how to succeed in the course

In-class participation is important (it implies attendance importance).
Topic-based regular home-made assignment are major grading item.
Please be aware that the lecture materials cover a plenty of topics from many sources, not a single one.

Resources, literature and reference materials

Open access resources

  • Dijkstra E.W. A Discipline of Programming. Prentice-Hal, 1976.
  • Gries D. The Science of Programming. Springer, 1987.
  • Aaby A. Introduction to Programming Language. Working draft, 2004. Available at .
  • Barendregt H. Lambda Calculi with Types. In: Handbook of Logic in Computer Science. Oxford University Press, 1992. Vol. II, pp. 117-309. Available at ftp://ftp.cs.ru.nl/pub/CompMath.Found/HBK.ps.
  • Shilov N.V. Introduction to Program Syntax, Semantics and Verification. (In Russian.) Novosibirsk State University, 2011. Draft is available at .

Closed access resources

  • Not needed.

Software and tools used within the course

  • Any compiler and IDE to implement, test, and exercise simple computational, search and sorting imperative and functional algorithms/programs.

Teaching Methodology: Methods, techniques, & activities

Activities and Teaching Methods

Teaching and Learning Methods within each section
Teaching Techniques Section 1 Section 2 Section 3 Section 4 Section 5
Problem-based learning (students learn by solving open-ended problems without a strictly defined solution) 1 1 1 1 1
Differentiated learning (provide tasks and activities at several levels of difficulty to fit students needs and level) 1 1 1 1 1
Contextual learning (activities and tasks are connected to the real world to make it easier for students to relate to them); 1 1 1 1 1
Развивающее обучение (задания и материал "прокачивают" ещё нераскрытые возможности студентов); 1 1 1 1 1
Концентрированное обучение (занятия по одной большой теме логически объединяются); 1 1 1 1 1
Activities within each section
Learning Activities Section 1 Section 2 Section 3 Section 4 Section 5
Lectures 1 1 1 1 1
Interactive Lectures 1 1 1 1 1
Lab exercises 1 1 1 1 1
Flipped classroom 1 1 1 1 1
Quizzes (written or computer based) 1 1 1 1 1
Discussions 1 1 1 1 1

Formative Assessment and Course Activities

Ongoing performance assessment

Section 1

Activity Type Content Is Graded?
Home-made problem-solving assignment Assume that , , and are sets.
Prove without use of the power-set axiom that is a set.
Prove without use of the set-union axiom that is a set.
Prove (using extensionality postulate)
uniqueness of the empty set
uniqueness of the set for any given finite collection of sets of , … .
Proof (using the enumeration and union postulate) existence of the standard union for all sets and .
Proof (using the specification postulate) existence of the standard intersection for all sets and .
Prove that for any set and any its subset the complement is a set.
Proof (by contradiction using specification axiom) that collection usually called as the set of all sets isn’t a set. (Russel’s paradox.)		 1

Section 2

Activity Type Content Is Graded?
Home-made problem-solving assignment Is TEL a regular language? A context-free language? A context-sensitive language? A Recursively enumerable language?
What will happen with TEL syntax (in terms of Chomsky classification) if it adopts spacing and indentation like Python?
Assuming that all variables are of integer type and a conventional semantics for program answer what does this program compute?
Validate that is indeed the operational semantics of TEL sentence .
Prove that in TEL the following sentences and are equivalent.
Prove that and are not equivalent in TEL.		 1

Section 3

Activity Type Content Is Graded?
Home-made problem-solving assignment Is ToyPL-VM language a context-free? Does it have a context-free syntax?
Assuming a conventional program semantics and that the only data type is mathematical integers, try to guess (and prove somehow) what does compute the following ToyPL-VM program:
0: if z<0 then 1 else 2;
1: z:= -1 goto 8;
2: x:= 0 goto 3;
3: y:= 0 goto 4;
4: if y≤z then 5 else 7;
5: y:= y+2*x+1 goto 6;
6: x:= x+1 goto 4;
7: x:= x-1 goto 8;
Let be any ToyPL-VM program, be any state of . Define by induction on structure of the expression (that uses variables in only) the value of this expression in this state .
Let be any ToyPL-VM program, be any state of . Prove by induction on structure of the expression that for any expression (based on variables in ) the value of this expression in this state has a definite value.
Validate that the implementation (semantics) of the ToyPL program from the left column is the ToyPL-VM program in right column.
Select (always) valid assertions and explain your choice:
 1

Section 4

Activity Type Content Is Graded?
Home-made problem-solving assignment Is the language of the -Calculus regular? Context-free?
The following sugared -term is representation of the following -term:





List all free and bound variable instances in the -terms (a)-(e) from the previous exercise. Which of these -terms are combinators?
Assuming the sugaring has no precedence, whether the desugaring of the -terms is confluent (i.e., always end with the same term)?
Assuming the sugaring has the specified precedence, whether the desugaring of the -terms is confluent (i.e., always end with the same term)?
Explain the following “proof” in the axiomatic semantics of the -Calculus and find a breach of the semantics:
 1

Section 5

Activity Type Content Is Graded?
Home-made problem-solving assignment Suggest any fix-point combinator other than .
Write a Java-, Python-, etc. program that (being aware about its location) prints out its own code.
Write yourself a quine-program in Java, Python, etc.
Give example of a -term such that has a reduction graph that
is a singleton with a single edge
is a finite chain of length
is an infinite chain
Prove Church-Rosser theorem: If there are two distinct (-)reductions starting from a -term, then there exists a -term that is reachable from both reducts via a (possibly empty) sequence of (-)reductions.
What is true:
If a -term has a normal form, then its reduction graph is finite.
If a -term has a finite reduction graph, then it has a normal form.
Proof by induction of the height of the inference tree soundness of the axiomatic semantic of -Calculus: For any -terms and , if then there exists -term such that and .		 1

Final assessment

Section 1

  1. Can be a final exam, project defense, or some other equivalent of the final exam.
  2. The final examination is distance asynchronous individual written test to check that students understand and can apply main definitions, concepts and techniques presented on the lectures and available in lecture notes. The main grading criterions for written test will be human readable but concise, self-completeness, well-structuredness, and “proof of individual work” while computational (mainly arithmetic) errors will be treated as tiny mistakes (at most one-point deduction for each individual task).
  3. Examination has one (parameterized) variant for all enrolled students with 5 tasks with cost 8 points each (i.e., 40 points in total). “Human readable but concise” rule means that solutions should be well-commented but not exciding 1.5 (one and a half) pages each. Self-completeness means that the paper should be readable independently on any other resource, but lecture notes. Well-structuredness means that each task formulation, solution (proof if needed), answer (or conclusion) and its parts must be explicit in the paper and identified by appropriate headings/keywords (with respect to logical structure).
  4. Sample tasks follow.
  5. Task 1. Using definition of the natural number as in the lecture notes for section 1, construct the powerset for a given (specified) natural number . How many elements does it (the powerset) contains? (Explain all your answers.)
  6. Task 2. Using definitions from the lecture notes for section 2, construct a TEL “meaningful program” that after evaluation according to TEL informal semantics gets value , construct (step by step) its operational, denotational, and axiomatic semantics according to the TEL definitions. Here “meaningful” means that you can explain what does the program computes assuming a conventional informal program semantics. Please explain informally what this semantics is.
  7. Task 3. Using definitions from the lecture notes for section 3, and the same program as you construct in the exercise 2 above, construct (step by step) its operational and denotational semantics as a ToyPL program.
  8. Task 4. Using definitions from the lecture notes for section 3, and the same program as you construct in the exercise 2 above, specify the program by pre- and post-conditions according to your explanations (in the exercise 2) of what does the program compute, and then verify (using Floyd method or Hoare axiomatic semantics) correctness of the specified program.
  9. Task 5. Using definitions from the lecture notes for sections 4 & 5, construct a given (specified) natural number . Whether it is a combinator? Build reduction graph for . (Explain all your answers.)

Section 2

Section 3

Section 4

Section 5


The retake exam

Section 1

  1. Retake and re-examinations are designed to check that students understand and can apply main definitions, concepts and techniques covered in the lectures of the Course to overwrite grades for the final examination.
  2. Hybrid re-examination mode means that the examinations comprise a distance asynchronous individual written test (the first re-examination to be graded by Prof. N.V. Shilov) and an oral defense in front of a commission (consisting of Prof. N.V. Shilov and two more faculty to be appointed by the time of the second re-examination); format of the oral defense – offline or online – to be decided/arranged later (but prior to the defense date to be set by the Department of Education).
  3. Since (according to the Syllabus available the final examination costs 40 points, the cost of the re-examination is also 40 points. So, individual overall grade for the course after the retake for each participating student will be calculated according to the following formula , where is student’ overall score earned for the course during the teaching term, is student’ overall score earned for the final examination, is student’ score earned for the re-examination.
  4. Examination set comprises 5 individual tasks (but the same for both retakes) with cost points each (i.e., 40 points in total). “Human readable but concise” rule means that solutions should be well-commented but not exciding 1.5 (one and a half) pages each. Self-completeness means that the paper should be readable independently on any other resource, but lecture notes. Well-structuredness means that each task formulation, solution (proof if needed), answer (or conclusion) and its parts must be explicit in the paper and identified by appropriate headings/keywords (with respect to logical structure).
  5. Sample tasks follow.
  6. Task 1. Let us assume that ‘’, ‘‘, ‘’, and ‘’ are symbols. Using definition of the natural number as in the lecture notes on the topic 1, count (ignoring blank spaces) the length of the string thar represents a given natural number . How many elements does this representation contains? (Explain all your answers.)
  7. Task 2. Using definitions from the lecture notes on the topic 2, construct a TEL-program that in conventional (natural for a programming language) semantics computes (outputs) the integer part of the square root of a (input) positive integer, but that after evaluation according to TEL informal semantics gets value for a given natural number , construct (step by step) its operational, denotational, and axiomatic semantics according to the TEL definitions.
  8. Task 3. Using definitions from the lecture notes on the topic 3, and the same program as you construct in the exercise 2 above, construct (step by step) its implementation and denotational semantics as a ToyPL program.
  9. Task 4. Using definitions from the lecture notes on the topic 3, and the same program as you construct in the exercise 2 above, specify the program by pre- and post-conditions according to your explanations (in the exercise 2) of what does the program compute, and then verify (using Floyd method or Hoare axiomatic semantics) correctness of the specified program.
  10. Task 5. Using definitions from the lecture notes on the topics 4 and 5, construct explicitly the numeral for a given natural number . What is type of the numeral Demonstrate that . What is type of the term ? Build reduction graph for . (Explain all your answers.)

Section 2

Section 3

Section 4

Section 5

Retrieved from "https://eduwiki.innopolis.university/index.php?title=IU:TestPage&oldid=8085"