Приложение одной разновидности типизированного λ-исчисления к построению формальных моделей программдоклад на конференции